let n be Nat; :: thesis:
let a, b be Element of REAL n; :: thesis:
thus OpenHyperInterval (a,b) c= LeftOpenHyperInterval (a,b) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in OpenHyperInterval (a,b) ; :: thesis:
then consider y being Element of REAL n such that
A1: x = y and
A2: for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ by Def4;

now :: thesis:

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
then ( y . i in ].(a . i),(b . i).[ & ].(a . i),(b . i).[ c= ].(a . i),(b . i).] ) by A2, XXREAL_1:21;
hence y . i in ].(a . i),(b . i).] ; :: thesis:

end;

hence x in LeftOpenHyperInterval (a,b) by A1, Def5; :: thesis:

end;

thus OpenHyperInterval (a,b) c= RightOpenHyperInterval (a,b) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in OpenHyperInterval (a,b) ; :: thesis:
then consider y being Element of REAL n such that
A3: x = y and
A4: for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ by Def4;

now :: thesis:

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
then ( y . i in ].(a . i),(b . i).[ & ].(a . i),(b . i).[ c= [.(a . i),(b . i).[ ) by A4, XXREAL_1:22;
hence y . i in [.(a . i),(b . i).[ ; :: thesis:

end;

hence x in RightOpenHyperInterval (a,b) by A3, Def6; :: thesis:

end;

thus LeftOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in LeftOpenHyperInterval (a,b) ; :: thesis:
then consider y being Element of REAL n such that
A5: x = y and
A6: for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] by Def5;

now :: thesis:

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
then ( y . i in ].(a . i),(b . i).] & ].(a . i),(b . i).] c= [.(a . i),(b . i).] ) by A6, XXREAL_1:23;
hence y . i in [.(a . i),(b . i).] ; :: thesis:

end;

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

end;

thus RightOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in RightOpenHyperInterval (a,b) ; :: thesis:
then consider y being Element of REAL n such that
A7: x = y and
A8: for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ by Def6;

now :: thesis:

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
then ( y . i in [.(a . i),(b . i).[ & [.(a . i),(b . i).[ c= [.(a . i),(b . i).] ) by A8, XXREAL_1:24;
hence y . i in [.(a . i),(b . i).] ; :: thesis:

end;

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

end;