let a, b be real number ; :: 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 convex by A1, Th13;
hence the carrier of (pi_1 (Closed-Interval-TSpace a,b),x) = {(Class (EqRel (Closed-Interval-TSpace a,b),x),C)} by Th17; :: thesis: verum