let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n ex P being Element of plane_of_REAL n st
( x in P & L c= P )
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n ex P being Element of plane_of_REAL n st
( x in P & L c= P )
let L be Element of line_of_REAL n; :: thesis: ex P being Element of plane_of_REAL n st
( x in P & L c= P )
L in line_of_REAL n ;
then consider L0 being Subset of (REAL n) such that
A1: ( L = L0 & ex x1, x2 being Element of REAL n st L0 = Line x1,x2 ) ;
consider x1, x2 being Element of REAL n such that
A2: L = Line x1,x2 by A1;
reconsider P = plane x,x1,x2 as Subset of (REAL n) ;
A3: ( x in P & x1 in P & x2 in P ) by Th87;
take P ; :: thesis: ( P is Element of plane_of_REAL n & x in P & L c= P )
thus ( P is Element of plane_of_REAL n & x in P & L c= P ) by A2, A3, Th90, Th95; :: thesis: verum