let n be Element of 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 ) by Def12;
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, Th95; :: thesis: verum

end;

now

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, Def12; :: 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