for T being TopStruct
for a, b being Real st a > b holds
[.a,b.] is empty compact Subset of T