for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for P, Q being Path of a,b holds
( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic )