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

hence ( I[01] is compact & I[01] is T_2 ) by HEINE:4, PCOMPS_1:34, TOPMETR:20; :: thesis: verum