let n be Nat; :: thesis: for a being Element of REAL n holds ClosedHyperInterval (a,a) = {a}
let a be Element of REAL n; :: thesis: ClosedHyperInterval (a,a) = {a}
A1: ClosedHyperInterval (a,a) c= {a}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ClosedHyperInterval (a,a) or x in {a} )
assume x in ClosedHyperInterval (a,a) ; :: thesis: x in {a}
then consider y being Element of REAL n such that
A2: x = y and
A3: for i being Nat st i in Seg n holds
y . i in [.(a . i),(a . i).] by Def3;
reconsider y1 = y, a1 = a as Function ;
A4: ( dom y = Seg n & dom a1 = Seg n ) by FINSEQ_2:124;
for z being object st z in dom y1 holds
y1 . z = a1 . z

proof

let z be object ; :: thesis: ( z in dom y1 implies y1 . z = a1 . z )
assume z in dom y1 ; :: thesis: y1 . z = a1 . z
then z in Seg n by FINSEQ_2:124;
then y1 . z in [.(a . z),(a . z).] by A3;
then y1 . z in {(a . z)} by XXREAL_1:17;
hence y1 . z = a1 . z by TARSKI:def 1; :: thesis: verum

end;

then y1 = a1 by A4, FUNCT_1:def 11;
hence x in {a} by A2, TARSKI:def 1; :: thesis: verum

end;

{a} c= ClosedHyperInterval (a,a)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} or x in ClosedHyperInterval (a,a) )
assume A5: x in {a} ; :: thesis: x in ClosedHyperInterval (a,a)
then reconsider x1 = x as Element of REAL n by TARSKI:def 1;
for i being Nat st i in Seg n holds
x1 . i in [.(a . i),(a . i).]

proof

let i be Nat; :: thesis: ( i in Seg n implies x1 . i in [.(a . i),(a . i).] )
assume i in Seg n ; :: thesis: x1 . i in [.(a . i),(a . i).]
x1 . i = a . i by A5, TARSKI:def 1;
then x1 . i in {(a . i)} by TARSKI:def 1;
hence x1 . i in [.(a . i),(a . i).] by XXREAL_1:17; :: thesis: verum

end;

hence x in ClosedHyperInterval (a,a) by Def3; :: thesis: verum

end;

hence ClosedHyperInterval (a,a) = {a} by A1; :: thesis: verum