for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n
for P being Element of plane_of_REAL n st x in P & L c= P & not x in L & L is being_line holds
P is being_plane