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: T is having_trivial_Fundamental_Group

for t being Point of T holds pi_1 (T,t) is trivial

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: T is having_trivial_Fundamental_Group

for t being Point of T holds pi_1 (T,t) is trivial

proof

hence
T is having_trivial_Fundamental_Group
; :: thesis: verum
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))}

end;set C = the constant Loop of t;

the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)), the constant Loop of t))}

proof

hence
pi_1 (T,t) is trivial
; :: thesis: verum
set E = EqRel (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 A4, EQREL_1:def 3;

hence x in the carrier of (pi_1 (T,t)) by TOPALG_1:def 5; :: thesis: verum

end;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 ; :: 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)) )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 A3, BORSUK_6:79;

then x = Class ((EqRel (T,t)), the constant Loop of t) by A2, TOPALG_1:46;

hence x in {(Class ((EqRel (T,t)), the constant Loop of t))} by TARSKI:def 1; :: thesis: verum

end;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 A3, BORSUK_6:79;

then x = Class ((EqRel (T,t)), the constant Loop of t) by A2, TOPALG_1:46;

hence x in {(Class ((EqRel (T,t)), the constant Loop of t))} by TARSKI:def 1; :: thesis: verum

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 A4, EQREL_1:def 3;

hence x in the carrier of (pi_1 (T,t)) by TOPALG_1:def 5; :: thesis: verum