let d be non zero Nat; for l, r, l9, r9 being Element of REAL d st ( for i being Element of Seg d holds l9 . i <= r9 . i ) holds
( cell (l,r) c= cell (l9,r9) iff for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) )
let l, r, l9, r9 be Element of REAL d; ( ( for i being Element of Seg d holds l9 . i <= r9 . i ) implies ( cell (l,r) c= cell (l9,r9) iff for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ) )
assume A1:
for i being Element of Seg d holds l9 . i <= r9 . i
; ( cell (l,r) c= cell (l9,r9) iff for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) )
thus
( cell (l,r) c= cell (l9,r9) implies for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) )
( ( for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ) implies cell (l,r) c= cell (l9,r9) )
assume A9:
for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i )
; cell (l,r) c= cell (l9,r9)
let x be object ; TARSKI:def 3 ( not x in cell (l,r) or x in cell (l9,r9) )
assume A10:
x in cell (l,r)
; x in cell (l9,r9)
then reconsider x = x as Element of REAL d ;
hence
x in cell (l9,r9)
; verum