theorem :: TOPALG_2:15

for a, b being Real st a <= b holds
for x being Point of (Closed-Interval-TSpace (a,b))
for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}