for n being Nat
for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 holds
P = plane (x1,x2,x3)