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

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