theorem :: MFOLD_2:30

for n being Nat
for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TPlane (p,q) is n -manifold