let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 implies ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane ) )
assume that
A1: L1 is being_line and
A2: L2 is being_line and
A3: L1 <> L2 and
A4: L1 meets L2 ; :: thesis: ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
consider x being Element of REAL n such that
A5: x in L1 and
A6: not x in L2 by A1, A2, A3, Th79;
A7: ex P being Element of plane_of_REAL n st
( x in P & L2 c= P & P is being_plane ) by A2, A6, Th100;
consider y being Element of REAL n such that
A8: y in L1 and
A9: y in L2 by A4, Th49;
L1 = Line (x,y) by A1, A5, A6, A8, A9, Th30;
hence ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane ) by A7, A9, Th95; :: thesis: verum