let T be non empty TopSpace; :: thesis: ( T is trivial implies T is having_trivial_Fundamental_Group )
assume A1: T is trivial ; :: thesis: T is having_trivial_Fundamental_Group
let t be Point of T; :: according to TOPALG_6:def 1 :: thesis: pi_1 (T,t) is trivial
reconsider L = I[01] --> t as Loop of t by JORDAN:41;
the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)),L))} by A1, Th8;
hence pi_1 (T,t) is trivial ; :: thesis: verum