let n be Nat; :: thesis: for a, b, c, d being Element of REAL n st a <= c & d <= b holds
ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b)
let a, b, c, d be Element of REAL n; :: thesis: ( a <= c & d <= b implies ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b) )
assume that
A1: a <= c and
A3: d <= b ; :: thesis: ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b)

now :: thesis: for t being object st t in ClosedHyperInterval (c,d) holds
t in ClosedHyperInterval (a,b)

let t be object ; :: thesis: ( t in ClosedHyperInterval (c,d) implies t in ClosedHyperInterval (a,b) )
assume t in ClosedHyperInterval (c,d) ; :: thesis: t in ClosedHyperInterval (a,b)
then consider t1 being Element of REAL n such that
A4: t = t1 and
A5: for i being Nat st i in Seg n holds
t1 . i in [.(c . i),(d . i).] by Def3;
for i being Nat st i in Seg n holds
t1 . i in [.(a . i),(b . i).]

proof

let i be Nat; :: thesis: ( i in Seg n implies t1 . i in [.(a . i),(b . i).] )
assume A6: i in Seg n ; :: thesis: t1 . i in [.(a . i),(b . i).]
then ( a . i <= c . i & d . i <= b . i ) by A1, A3;
then [.(c . i),(d . i).] c= [.(a . i),(b . i).] by XXREAL_1:34;
hence t1 . i in [.(a . i),(b . i).] by A6, A5; :: thesis: verum

end;

hence t in ClosedHyperInterval (a,b) by A4, Def3; :: thesis: verum

end;

hence ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b) ; :: thesis: verum