:: deftheorem defines plane_of_REAL EUCLIDLP:def 11 :
for n being Nat holds plane_of_REAL n = { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ;