let d be non zero Nat; :: thesis: for l, r being Element of REAL d holds
( l in cell (l,r) & r in cell (l,r) )
let l, r be Element of REAL d; :: thesis: ( l in cell (l,r) & r in cell (l,r) )
A1: ( for i being Element of Seg d holds
( l . i <= l . i & l . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i & ( l . i <= r . i or l . i <= l . i ) ) ) ;
( for i being Element of Seg d holds
( l . i <= r . i & r . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i & ( r . i <= r . i or l . i <= r . i ) ) ) ;
hence ( l in cell (l,r) & r in cell (l,r) ) by A1; :: thesis: verum