assume [L1,L2,A,N1,N2] : (line(L1) & line(L2) & point(A) & line(N1) & line(N2) & ninc_po_l(A,L1) & ninc_po_l(A,L2) & N1!=N2 & inc_po_l(A,N1) & inc_po_l(A,N2) & int_l_l(N1,L1) & int_l_l(N1,L2) & int_l_l(N2,L1) & int_l_l(N2,L2))
let [B1] : (point(B1) & inc_po_l(B1,N1) & inc_po_l(B1,L1))
let [C1] : (point(C1) & inc_po_l(C1,N2) & inc_po_l(C1,L1))
let [B2] : (point(B2) & inc_po_l(B2,N1) & inc_po_l(B2,L2))
let [C2] : (point(C2) & inc_po_l(C2,N2) & inc_po_l(C2,L2))
have (ncol(A,B1,C1))
let [P] : (plane(P) & inc_po_pl(A,P) & inc_po_pl(B1,P) & inc_po_pl(C1,P))
have (inc_l_pl(N1,P) & inc_l_pl(N2,P))
have (inc_l_pl(L1,P) & inc_l_pl(L2,P))
