for X being non empty TopSpace
for a being Point of X
for x, y being Element of (pi_1 (X,a))
for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds
x " = y