let d be non zero Nat; :: thesis: for l, r, x being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) holds

( x in cell (l,r) iff for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) )

let l, r, x be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l . i <= r . i ) implies ( x in cell (l,r) iff for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) ) )

assume A1: for i being Element of Seg d holds l . i <= r . i ; :: thesis: ( x in cell (l,r) iff for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) )

( l . i <= x . i & x . i <= r . i ) ) implies x in cell (l,r) ) ; :: thesis: verum

( x in cell (l,r) iff for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) )

let l, r, x be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l . i <= r . i ) implies ( x in cell (l,r) iff for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) ) )

assume A1: for i being Element of Seg d holds l . i <= r . i ; :: thesis: ( x in cell (l,r) iff for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) )

hereby :: thesis: ( ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) ) implies x in cell (l,r) )

thus
( ( for i being Element of Seg d holds ( l . i <= x . i & x . i <= r . i ) ) implies x in cell (l,r) )

assume
x in cell (l,r)
; :: thesis: for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i )

then ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st

( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) by Th20;

hence for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) by A1; :: thesis: verum

end;( l . i <= x . i & x . i <= r . i )

then ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st

( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) by Th20;

hence for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) by A1; :: thesis: verum

( l . i <= x . i & x . i <= r . i ) ) implies x in cell (l,r) ) ; :: thesis: verum