let T be TopStruct ; :: thesis: for a, b being real number st a > b holds
[.a,b.] is empty compact Subset of T
let a, b be real number ; :: thesis: ( a > b implies [.a,b.] is empty compact Subset of T )
assume a > b ; :: thesis: [.a,b.] is empty compact Subset of T
then [.a,b.] = {} T by XXREAL_1:29;
hence [.a,b.] is empty compact Subset of T ; :: thesis: verum