let X be non empty TopSpace; :: thesis: for a being Point of X ex E being Equivalence_Relation of Loops a st
for x, y being set holds
( [x,y] in E iff ( x in Loops a & y in Loops a & ex P, Q being Loop of a st
( P = x & Q = y & P,Q are_homotopic ) ) )
let a be Point of X; :: thesis: ex E being Equivalence_Relation of Loops a st
for x, y being set holds
( [x,y] in E iff ( x in Loops a & y in Loops a & ex P, Q being Loop of a st
( P = x & Q = y & P,Q are_homotopic ) ) )
defpred S₁[ set , set ] means ex P, Q being Loop of a st
( P = $1 & Q = $2 & P,Q are_homotopic );
A1: for x being set st x in Loops a holds
S₁[x,x]

proof

let x be set ; :: thesis: ( x in Loops a implies S₁[x,x] )
assume x in Loops a ; :: thesis: S₁[x,x]
then reconsider x = x as Loop of a by Def1;
x,x are_homotopic by BORSUK_2:15;
hence S₁[x,x] ; :: thesis: verum

end;

A2: for x, y being set st S₁[x,y] holds
S₁[y,x] ;
A3: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by BORSUK_6:87;
thus ex EqR being Equivalence_Relation of Loops a st
for x, y being set holds
( [x,y] in EqR iff ( x in Loops a & y in Loops a & S₁[x,y] ) ) from EQREL_1:sch 1(A1, A2, A3); :: thesis: verum