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

( 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