let X be non empty TopSpace; :: thesis: for a, b being Point of X st a,b are_connected holds
ex E being Equivalence_Relation of (Paths (a,b)) st
for x, y being object holds
( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) )
let a, b be Point of X; :: thesis: ( a,b are_connected implies ex E being Equivalence_Relation of (Paths (a,b)) st
for x, y being object holds
( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) ) )
assume A1: a,b are_connected ; :: thesis: ex E being Equivalence_Relation of (Paths (a,b)) st
for x, y being object holds
( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) )
defpred S₁[ object , object ] means ex P, Q being Path of a,b st
( P = $1 & Q = $2 & P,Q are_homotopic );
A2: for x being object st x in Paths (a,b) holds
S₁[x,x]

proof

let x be object ; :: thesis: ( x in Paths (a,b) implies S₁[x,x] )
assume x in Paths (a,b) ; :: thesis: S₁[x,x]
then reconsider x = x as Path of a,b by Def1;
x,x are_homotopic by A1, BORSUK_2:12;
hence S₁[x,x] ; :: thesis: verum

end;

A3: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by BORSUK_6:79;
A4: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
thus ex EqR being Equivalence_Relation of (Paths (a,b)) st
for x, y being object holds
( [x,y] in EqR iff ( x in Paths (a,b) & y in Paths (a,b) & S₁[x,y] ) ) from EQREL_1:sch 1(A2, A4, A3); :: thesis: verum