theorem Th13: :: TOPALG_2:13

for T being non empty interval SubSpace of R^1
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))}