let n be Nat; 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; ( a <= c & d <= b implies ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b) )
assume that
A1:
a <= c
and
A3:
d <= b
; ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b)
hence
ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b)
; verum