let X be non empty TopSpace; :: thesis: for a, b being Point of X st a,b are_connected holds
for P, Q being Path of a,b holds
( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic )
let a, b be Point of X; :: thesis: ( a,b are_connected implies for P, Q being Path of a,b holds
( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic ) )
set E = EqRel (X,a,b);
assume A1: a,b are_connected ; :: thesis: for P, Q being Path of a,b holds
( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic )
let P, Q be Path of a,b; :: thesis: ( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic )
A2: Q in Paths (a,b) by Def1;
A3: ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by A1, Lm3;

hereby :: thesis: ( P,Q are_homotopic implies Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) )

assume Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) ; :: thesis: P,Q are_homotopic
then P in Class ((EqRel (X,a,b)),Q) by A3, A2, EQREL_1:23;
hence P,Q are_homotopic by A1, Th45; :: thesis: verum

end;

assume P,Q are_homotopic ; :: thesis: Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q)
then P in Class ((EqRel (X,a,b)),Q) by A1, Th45;
hence Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) by A3, A2, EQREL_1:23; :: thesis: verum