let X be non empty TopSpace; 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; ( 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
; 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 S1[ 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
S1[x,x]
A3:
for x, y, z being object st S1[x,y] & S1[y,z] holds
S1[x,z]
by BORSUK_6:79;
A4:
for x, y being object st S1[x,y] holds
S1[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) & S1[x,y] ) )
from EQREL_1:sch 1(A2, A4, A3); verum