I[01] = TopSpaceMetr (Closed-Interval-MSpace 0 ,1) by TOPMETR:27, TOPMETR:def 8;
hence ( I[01] is compact & I[01] is T_2 ) by HEINE:11, PCOMPS_1:38, TOPMETR:27; :: thesis: verum