let n be Element of NAT ; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( P is being_plane & L1 c= P & L2 c= P )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 _|_ L2 & L1 meets L2 implies ex P being Element of plane_of_REAL n st
( P is being_plane & L1 c= P & L2 c= P ) )
assume that
A1: L1 _|_ L2 and
A2: L1 meets L2 ; :: thesis: ex P being Element of plane_of_REAL n st
( P is being_plane & L1 c= P & L2 c= P )
consider x1 being Element of REAL n such that
A3: x1 in L1 and
A4: x1 in L2 by A2, Th54;
L1 is being_line by A1, Th72;
then consider x2 being Element of REAL n such that
A5: ( x2 <> x1 & x2 in L1 ) by Th58;
A6: L1 = Line x1,x2 by A3, A5, Th69;
L2 is being_line by A1, Th72;
then consider x3 being Element of REAL n such that
A7: ( x3 <> x1 & x3 in L2 ) by Th58;
reconsider P = plane x1,x2,x3 as Subset of (REAL n) ;
take P ; :: thesis: ( P is Element of plane_of_REAL n & P is being_plane & L1 c= P & L2 c= P )
A8: ( x1 in P & x2 in P ) by Th87;
A9: x3 in P by Th87;
A10: L2 = Line x1,x3 by A4, A7, Th69;
x2 - x1,x3 - x1 are_lindependent2 by A1, A3, A4, A5, A7, Th50, Th79;
hence ( P is Element of plane_of_REAL n & P is being_plane & L1 c= P & L2 c= P ) by A6, A10, A8, A9, Def10, Th90, Th95; :: thesis: verum