assume [L1,L2,L3,A,B,C] : (line(L1) & line(L2) & line(L3) & point(A) & point(B) & point(C) & L1!=L2 & L2!=L3 & L3!=L1 & int_l_l(L1,L2) & int_l_l(L2,L3) & int_l_l(L3,L1) & inc_po_l(A,L1) & inc_po_l(A,L2) & ninc_po_l(A,L3) & ninc_po_l(B,L1) & inc_po_l(B,L2) & inc_po_l(B,L3) & inc_po_l(C,L1) & ninc_po_l(C,L2) & inc_po_l(C,L3))
let [P] : (plane(P) & inc_po_pl(A,P) & inc_po_pl(B,P) & inc_po_pl(C,P))
have (inc_l_pl(L1,P) & inc_l_pl(L2,P) & inc_l_pl(L3,P))
