let T be TopStruct ; :: thesis: for a, b being Real st a > b holds
[.a,b.] is empty compact Subset of T
let a, b be Real; :: 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