let n be 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, Th49;
L1 is being_line by A1, Th67;
then consider x2 being Element of REAL n such that
A5: ( x2 <> x1 & x2 in L1 ) by Th53;
A6: L1 = Line (x1,x2) by A3, A5, Th64;
L2 is being_line by A1, Th67;
then consider x3 being Element of REAL n such that
A7: ( x3 <> x1 & x3 in L2 ) by Th53;
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 Th82;
A9: x3 in P by Th82;
A10: L2 = Line (x1,x3) by A4, A7, Th64;
x2 - x1,x3 - x1 are_lindependent2 by A1, A3, A4, A5, A7, Th45, Th74;
hence ( P is Element of plane_of_REAL n & P is being_plane & L1 c= P & L2 c= P ) by A6, A10, A8, A9, Th85, Th90; :: thesis: verum