let n be Nat; :: thesis: for a, b being Element of REAL n st a <= b holds
not ClosedHyperInterval (a,b) is empty
let a, b be Element of REAL n; :: thesis: ( a <= b implies not ClosedHyperInterval (a,b) is empty )
assume a <= b ; :: thesis: not ClosedHyperInterval (a,b) is empty
then ClosedHyperInterval (a,a) c= ClosedHyperInterval (a,b) by Th49;
then {a} c= ClosedHyperInterval (a,b) by Th48;
hence not ClosedHyperInterval (a,b) is empty ; :: thesis: verum