I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def 7;
hence ( I[01] is compact & I[01] is T_2 ) by HEINE:4, PCOMPS_1:34, TOPMETR:20; :: thesis: verum