b in [.a,b.] by A1, XXREAL_1:1;
hence b is Point of (Closed-Interval-TSpace a,b) by A1, TOPMETR:25; :: thesis: verum