let T be non empty TopSpace; :: thesis: ( ( for t being Point of T
for f being Loop of t holds f is nullhomotopic ) implies T is having_trivial_Fundamental_Group )

assume A1: for t being Point of T
for f being Loop of t holds f is nullhomotopic ; :: thesis:
for t being Point of T holds pi_1 (T,t) is trivial
proof
let t be Point of T; :: thesis: pi_1 (T,t) is trivial
set C = the constant Loop of t;
the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)), the constant Loop of t))}
proof
set E = EqRel (T,t);
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Class ((EqRel (T,t)), the constant Loop of t))} c= the carrier of (pi_1 (T,t))
let x be object ; :: thesis: ( x in the carrier of (pi_1 (T,t)) implies x in {(Class ((EqRel (T,t)), the constant Loop of t))} )
assume x in the carrier of (pi_1 (T,t)) ; :: thesis: x in {(Class ((EqRel (T,t)), the constant Loop of t))}
then consider P being Loop of t such that
A2: x = Class ((EqRel (T,t)),P) by TOPALG_1:47;
P is nullhomotopic by A1;
then consider C1 being constant Loop of t such that
A3: P,C1 are_homotopic ;
C1, the constant Loop of t are_homotopic by Th5;
then P, the constant Loop of t are_homotopic by ;
then x = Class ((EqRel (T,t)), the constant Loop of t) by ;
hence x in {(Class ((EqRel (T,t)), the constant Loop of t))} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Class ((EqRel (T,t)), the constant Loop of t))} or x in the carrier of (pi_1 (T,t)) )
assume x in {(Class ((EqRel (T,t)), the constant Loop of t))} ; :: thesis: x in the carrier of (pi_1 (T,t))
then A4: x = Class ((EqRel (T,t)), the constant Loop of t) by TARSKI:def 1;
the constant Loop of t in Loops t by TOPALG_1:def 1;
then x in Class (EqRel (T,t)) by ;
hence x in the carrier of (pi_1 (T,t)) by TOPALG_1:def 5; :: thesis: verum
end;
hence pi_1 (T,t) is trivial ; :: thesis: verum
end;
hence T is having_trivial_Fundamental_Group ; :: thesis: verum