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:18;
hence x is Real by Lm1; :: thesis: verum