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 ) )
hereby :: thesis: ( ( 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;
thus ( ( for i being Element of Seg d holds
( l . i <= x . i & x . i <= r . i ) ) implies x in cell (l,r) ) ; :: thesis: verum