let X be non empty TopSpace; 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; ( 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
; 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; ( 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 ( 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)
;
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;
verum
end;
assume
P,Q are_homotopic
; 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; verum