let n be Nat; :: thesis: for a, b being Element of REAL n st b < a & not n is zero holds
ClosedHyperInterval (a,b) is empty
let a, b be Element of REAL n; :: thesis: ( b < a & not n is zero implies ClosedHyperInterval (a,b) is empty )
assume that
A1: b < a and
A2: not n is zero ; :: thesis: ClosedHyperInterval (a,b) is empty
assume not ClosedHyperInterval (a,b) is empty ; :: thesis: contradiction
then consider x being object such that
A3: x in ClosedHyperInterval (a,b) ;
consider y being Element of REAL n such that
x = y and
A4: for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] by A3, Def3;
1 <= n by A2, NAT_1:14;
then ( b . 1 < a . 1 & y . 1 in [.(a . 1),(b . 1).] ) by A1, A4, FINSEQ_1:1;
hence contradiction by XXREAL_1:29; :: thesis: verum