:: deftheorem Def3 defines EqRel TOPALG_1:def 3 :
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for b₄ being Relation of (Paths (a,b)) holds
( b₄ = EqRel (X,a,b) iff for P, Q being Path of a,b holds
( [P,Q] in b₄ iff P,Q are_homotopic ) );