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
( Q in Class (EqRel X,a,b),P 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
( Q in Class (EqRel X,a,b),P 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
( Q in Class (EqRel X,a,b),P iff P,Q are_homotopic )
let P, Q be Path of a,b; :: thesis: ( Q in Class (EqRel X,a,b),P iff P,Q are_homotopic )
A2: ( 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 Q in Class (EqRel X,a,b),P )

assume Q in Class (EqRel X,a,b),P ; :: thesis: P,Q are_homotopic
then [Q,P] in EqRel X,a,b by A2, EQREL_1:27;
hence P,Q are_homotopic by A1, Def3; :: thesis: verum

end;

assume P,Q are_homotopic ; :: thesis: Q in Class (EqRel X,a,b),P
then [Q,P] in EqRel X,a,b by A1, Def3;
hence Q in Class (EqRel X,a,b),P by A2, EQREL_1:27; :: thesis: verum