let a, b be real number ; :: thesis: ( a <= b implies for x, y being Point of (Closed-Interval-TSpace a,b)
for P, Q being Path of x,y holds P,Q are_homotopic )
assume A1: a <= b ; :: thesis: for x, y being Point of (Closed-Interval-TSpace a,b)
for P, Q being Path of x,y holds P,Q are_homotopic
let x, y be Point of (Closed-Interval-TSpace a,b); :: thesis: for P, Q being Path of x,y holds P,Q are_homotopic
let P, Q be Path of x,y; :: thesis: P,Q are_homotopic
Closed-Interval-TSpace a,b is interval by A1, Th13;
hence P,Q are_homotopic by Th16; :: thesis: verum