let n be Element of 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 A1: ( L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 ) ; :: thesis: ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
then consider x being Element of REAL n such that
A2: ( x in L1 & not x in L2 ) by Th84;
consider P being Element of plane_of_REAL n such that
A3: ( x in P & L2 c= P & P is being_plane ) by A1, A2, Th105;
consider y being Element of REAL n such that
A4: ( y in L1 & y in L2 ) by A1, Th54;
L1 = Line x,y by A1, A2, A4, Th35;
hence ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane ) by A3, A4, Th100; :: thesis: verum