fof(goal, conjecture,(![L1,L2]:(line(L1)&line(L2)&int_l_l(L1,L2))=>(?[P]:(plane(P)&inc_l_pl(L1,P)&inc_l_pl(L2,P))))).
