for N being non empty MetrStruct st N is Reflexive & N is triangle & TopSpaceMetr N is compact holds
N is totally_bounded