:: deftheorem defines being_plane EUCLIDLP:def 10 :
for n being Nat
for A being Subset of (REAL n) holds
( A is being_plane iff ex x1, x2, x3 being Element of REAL n st
( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) ) );