theorem Th60: :: TOPALG_1:60

for n being Nat
for a being Point of (TOP-REAL n)
for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}