for M being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr M is countably_compact holds
M is totally_bounded