assume [P1,A,B,C,L1,L2,L3,M,N,K] : (plane(P1) & point(A) & point(B) & point(C) & ninc_po_pl(A,P1) & ninc_po_pl(B,P1) & ninc_po_pl(C,P1) & ncol(A,B,C) & line(L1) & line(L2) & line(L3) & inc_po_l(A,L1) & inc_po_l(B,L1) & inc_po_l(B,L2) & inc_po_l(C,L2) & inc_po_l(C,L3) & inc_po_l(A,L3) & point(M) & point(N) & point(K) & inc_po_pl(M,P1) & inc_po_l(M,L1) & inc_po_pl(N,P1) & inc_po_l(N,L2) & inc_po_pl(K,P1) & inc_po_l(K,L3))
let [P2] : (plane(P2) & inc_po_pl(A,P2) & inc_po_pl(B,P2) & inc_po_pl(C,P2))
have (inc_l_pl(L1,P2))
have (inc_l_pl(L2,P2))
have (inc_l_pl(L3,P2))
have (inc_po_pl(M,P2) & inc_po_pl(N,P2) & inc_po_pl(K,P2))
let [L4] : (line(L4) & inc_l_pl(L4,P1) & inc_l_pl(L4,P2))
let [R,S] : (point(R) & point(S) & R!=S & inc_po_l(R,L4) & inc_po_l(S,L4))
have (inc_po_l(M,L4) & inc_po_l(N,L4) & inc_po_l(K,L4))
have (col(M,N,K))
