let T be non empty TopSpace; :: thesis: ( T is simply_connected iff for t1, t2 being Point of T holds
( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) )

hereby :: thesis: ( ( for t1, t2 being Point of T holds
( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) ) implies T is simply_connected )

assume A1: T is simply_connected ; :: thesis: for t1, t2 being Point of T holds
( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) )
let t1, t2 be Point of T; :: thesis: ( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) )
thus A2: t1,t2 are_connected by A1, BORSUK_2:def 3; :: thesis: for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q)
let P, Q be Path of t1,t2; :: thesis: Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q)
set E = EqRel (T,t1,t2);
A3: P,(P + (- Q)) + Q are_homotopic by A1, TOPALG_1:22;
set C = the constant Loop of t1;
P + (- Q), the constant Loop of t1 are_homotopic by A1, Th11;
then A4: (P + (- Q)) + Q, the constant Loop of t1 + Q are_homotopic by A1, BORSUK_6:76;
the constant Loop of t1 + Q,Q are_homotopic by A1, BORSUK_6:83;
then (P + (- Q)) + Q,Q are_homotopic by A4, BORSUK_6:79;
then P,Q are_homotopic by A3, BORSUK_6:79;
hence Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) by A2, TOPALG_1:46; :: thesis: verum

end;

assume A5: for t1, t2 being Point of T holds
( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) ; :: thesis: T is simply_connected
thus T is having_trivial_Fundamental_Group :: according to TOPALG_6:def 2 :: thesis: T is pathwise_connected

proof

let t be Point of T; :: according to TOPALG_6:def 1 :: thesis: pi_1 (T,t) is trivial
let x, y be Element of (pi_1 (T,t)); :: according to STRUCT_0:def 10 :: thesis: x = y
( ex P being Loop of t st x = Class ((EqRel (T,t)),P) & ex P being Loop of t st y = Class ((EqRel (T,t)),P) ) by TOPALG_1:47;
hence x = y by A5; :: thesis: verum

end;

thus T is pathwise_connected by A5; :: thesis: verum