let a, b be Real; :: 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, Th9;
hence P,Q are_homotopic by Th12; :: thesis: verum