let a, b be real number ; :: thesis: for x being Point of st a <= b holds
x is Real
let x be Point of ; :: 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