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 ex L0 being Subset of (REAL n) st
( L = L0 & ex x1, x2 being Element of REAL n st L0 = Line x1,x2 ) ;
then consider x1, x2 being Element of REAL n such that
A1: L = Line x1,x2 ;
reconsider P = plane x,x1,x2 as Subset of (REAL n) ;
take P ; :: thesis: ( P is Element of plane_of_REAL n & x in P & L c= P )
( x1 in P & x2 in P ) by Th87;
hence ( P is Element of plane_of_REAL n & x in P & L c= P ) by A1, Th87, Th90, Th95; :: thesis: verum