let n be Element of 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 ) )
assume A1: ( 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 )
consider P being Element of plane_of_REAL n such that
A2: ( x in P & L c= P ) by Th104;
consider x1, x2 being Element of REAL n such that
A3: ( L = Line x1,x2 & x - x1,x2 - x1 are_lindependent2 ) by A1, Th60;
( x1 in L & x2 in L ) by A3, EUCLID_4:10;
then A4: P = plane x1,x,x2 by A2, A3, Th97;
take P ; :: thesis: ( x in P & L c= P & P is being_plane )
thus ( x in P & L c= P & P is being_plane ) by A2, A3, A4, Def10; :: thesis: verum