let a, b be Real; :: thesis: ( 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 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: verum