let o be Point of (TOP-REAL n); :: according to TOPALG_6:def 1 :: thesis: pi_1 ((TOP-REAL n),o) is trivial
thus pi_1 ((TOP-REAL n),o) is trivial ; :: thesis: verum