let d be non zero Element of 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 )
( ( 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 ) ; :: thesis: verum