for X being non empty TopSpace
for a being Point of X
for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)