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