let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n holds
( L1,L2 are_coplane iff ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1,L2 are_coplane iff ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) )
thus ( L1,L2 are_coplane implies ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) ) :: thesis: ( ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) implies L1,L2 are_coplane )
proof
assume L1,L2 are_coplane ; :: thesis: ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P )
then consider x1, x2, x3 being Element of REAL n such that
A1: ( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) ;
set P = plane (x1,x2,x3);
take plane (x1,x2,x3) ; :: thesis: ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) )
thus ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) by A1, Th90; :: thesis: verum
end;
now :: thesis: ( ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) implies L1,L2 are_coplane )
assume ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) ; :: thesis: L1,L2 are_coplane
then consider P being Element of plane_of_REAL n such that
A2: ( L1 c= P & L2 c= P ) ;
P in plane_of_REAL n ;
then ex P9 being Subset of (REAL n) st
( P = P9 & ex x1, x2, x3 being Element of REAL n st P9 = plane (x1,x2,x3) ) ;
hence L1,L2 are_coplane by A2; :: thesis: verum
end;
hence ( ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) implies L1,L2 are_coplane ) ; :: thesis: verum