let n be Nat; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex P being Element of plane_of_REAL n st
( x in P & L c= P & P is being_plane )
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex P being Element of plane_of_REAL n st
( x in P & L c= P & P is being_plane )
let L be Element of line_of_REAL n; :: thesis: ( not x in L & L is being_line implies ex P being Element of plane_of_REAL n st
( x in P & L c= P & P is being_plane ) )
consider P being Element of plane_of_REAL n such that
A1: ( x in P & L c= P ) by Th99;
assume ( not x in L & L is being_line ) ; :: thesis: ex P being Element of plane_of_REAL n st
( x in P & L c= P & P is being_plane )
then consider x1, x2 being Element of REAL n such that
A2: L = Line (x1,x2) and
A3: x - x1,x2 - x1 are_lindependent2 by Th55;
take P ; :: thesis: ( x in P & L c= P & P is being_plane )
( x1 in L & x2 in L ) by A2, EUCLID_4:9;
then P = plane (x1,x,x2) by A1, A3, Th92;
hence ( x in P & L c= P & P is being_plane ) by A1, A3; :: thesis: verum