let a, b be Real; ( a <= b implies 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))} )
assume A1:
a <= b
; 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))}
let x be 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))}
let C be Loop of x; the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}
Closed-Interval-TSpace (a,b) is interval
by A1, Th9;
hence
the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}
by Th13; verum