let n be Nat; :: thesis:
let a, b, c, d be Element of REAL n; :: thesis:
assume that
A1: a <= c and
A3: d <= b ; :: thesis:

let t be object ; :: thesis:
assume t in ClosedHyperInterval (c,d) ; :: thesis:
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).]

let i be Nat; :: thesis:
assume A6: i in Seg n ; :: thesis:
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:

end;

end;