let n be Nat; :: thesis: for a, b being Element of REAL n holds
( OpenHyperInterval (a,b) c= LeftOpenHyperInterval (a,b) & OpenHyperInterval (a,b) c= RightOpenHyperInterval (a,b) & LeftOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) & RightOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) )
let a, b be Element of REAL n; :: thesis: ( OpenHyperInterval (a,b) c= LeftOpenHyperInterval (a,b) & OpenHyperInterval (a,b) c= RightOpenHyperInterval (a,b) & LeftOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) & RightOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) )
thus OpenHyperInterval (a,b) c= LeftOpenHyperInterval (a,b) :: thesis: ( OpenHyperInterval (a,b) c= RightOpenHyperInterval (a,b) & LeftOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) & RightOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHyperInterval (a,b) or x in LeftOpenHyperInterval (a,b) )
assume x in OpenHyperInterval (a,b) ; :: thesis: x in LeftOpenHyperInterval (a,b)
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: for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).]

let i be Nat; :: thesis: ( i in Seg n implies y . i in ].(a . i),(b . i).] )
assume i in Seg n ; :: thesis: y . i in ].(a . i),(b . i).]
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: verum

end;

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHyperInterval (a,b) or x in RightOpenHyperInterval (a,b) )
assume x in OpenHyperInterval (a,b) ; :: thesis: x in RightOpenHyperInterval (a,b)
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: for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[

let i be Nat; :: thesis: ( i in Seg n implies y . i in [.(a . i),(b . i).[ )
assume i in Seg n ; :: thesis: y . i in [.(a . i),(b . i).[
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: verum

end;

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LeftOpenHyperInterval (a,b) or x in ClosedHyperInterval (a,b) )
assume x in LeftOpenHyperInterval (a,b) ; :: thesis: x in ClosedHyperInterval (a,b)
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: for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).]

let i be Nat; :: thesis: ( i in Seg n implies y . i in [.(a . i),(b . i).] )
assume i in Seg n ; :: thesis: y . i in [.(a . i),(b . i).]
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: verum

end;

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in RightOpenHyperInterval (a,b) or x in ClosedHyperInterval (a,b) )
assume x in RightOpenHyperInterval (a,b) ; :: thesis: x in ClosedHyperInterval (a,b)
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: for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).]

let i be Nat; :: thesis: ( i in Seg n implies y . i in [.(a . i),(b . i).] )
assume i in Seg n ; :: thesis: y . i in [.(a . i),(b . i).]
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: verum

end;

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

end;