theorem Th31: :: BORSUK_6:31

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