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 are_coplane & L1 <> 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 are_coplane & L1 <> 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 & L1,L2 are_coplane & L1 <> L2 ) ; :: thesis: ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
( ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) & ex x being Element of REAL n st
( x in L2 & not x in L1 ) ) by A1, A2, Th79, Th96;
hence ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane ) by A1, Th101; :: thesis: verum