theorem Th3: :: TOPALG_2:3

for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}