let n be Nat; :: thesis: for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TPlane (p,q) is n -manifold
let p, q be Point of (TOP-REAL (n + 1)); :: thesis: ( p <> 0. (TOP-REAL (n + 1)) implies TPlane (p,q) is n -manifold )
assume p <> 0. (TOP-REAL (n + 1)) ; :: thesis: TPlane (p,q) is n -manifold
then TOP-REAL n, TPlane (p,q) are_homeomorphic by Th29;
hence TPlane (p,q) is n -manifold by Th12; :: thesis: verum