let n be 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 x1, x2 being Element of REAL n such that
A1: L = Line (x1,x2) ;
take P = plane (x,x1,x2); :: thesis: ( P is Element of plane_of_REAL n & x in P & L c= P )
( x1 in P & x2 in P ) by Th82;
hence ( P is Element of plane_of_REAL n & x in P & L c= P ) by A1, Th82, Th85, Th90; :: thesis: verum