:: deftheorem defines Plane MFOLD_2:def 2 :
for n being Nat
for p, q being Point of (TOP-REAL n) holds Plane (p,q) = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;