let a, b be real number ; :: thesis: for x being Point of (Closed-Interval-TSpace a,b) st a <= b holds
x is Real
let x be Point of (Closed-Interval-TSpace a,b); :: thesis: ( a <= b implies x is Real )
assume a <= b ; :: thesis: x is Real
then the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] by TOPMETR:25;
hence x is Real by Lm1; :: thesis: verum