let X be non empty TopSpace; :: thesis: for a being Point of X
for P, Q being Loop of a holds
( Class (EqRel X,a),P = Class (EqRel X,a),Q iff P,Q are_homotopic )
let a be Point of X; :: thesis: for P, Q being Loop of a holds
( Class (EqRel X,a),P = Class (EqRel X,a),Q iff P,Q are_homotopic )
let P, Q be Loop of a; :: thesis: ( Class (EqRel X,a),P = Class (EqRel X,a),Q iff P,Q are_homotopic )
set E = EqRel X,a;
A1: Q in Loops a by Def1;

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

assume Class (EqRel X,a),P = Class (EqRel X,a),Q ; :: thesis: P,Q are_homotopic
then P in Class (EqRel X,a),Q by A1, EQREL_1:31;
hence P,Q are_homotopic by Th46; :: thesis: verum

end;

assume P,Q are_homotopic ; :: thesis: Class (EqRel X,a),P = Class (EqRel X,a),Q
then P in Class (EqRel X,a),Q by Th46;
hence Class (EqRel X,a),P = Class (EqRel X,a),Q by A1, EQREL_1:31; :: thesis: verum