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