:: deftheorem defines TPlane MFOLD_2:def 3 :
for n being Nat
for p, q being Point of (TOP-REAL n) holds TPlane (p,q) = (TOP-REAL n) | (Plane (p,q));