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

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

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

end;

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