theorem Th8: :: TOPALG_6:8

for T being non empty trivial TopSpace
for t being Point of T
for L being Loop of t holds the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)),L))}