let A, A9 be Cell of d,G; :: thesis: ( ex l, r being Element of REAL d st

( A = cell (l,r) & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) & ex l, r being Element of REAL d st

( A9 = cell (l,r) & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) implies A = A9 )

given l, r being Element of REAL d such that A19: A = cell (l,r) and

A20: for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: ( for l, r being Element of REAL d holds

( not A9 = cell (l,r) or ex i being Element of Seg d st

( r . i < l . i implies not [(l . i),(r . i)] is Gap of G . i ) ) or A = A9 )

given l9, r9 being Element of REAL d such that A21: A9 = cell (l9,r9) and

A22: for i being Element of Seg d holds

( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ; :: thesis: A = A9

reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def3;

hence A = A9 by A19, A21, A23, FUNCT_2:63; :: thesis: verum

( A = cell (l,r) & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) & ex l, r being Element of REAL d st

( A9 = cell (l,r) & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) implies A = A9 )

given l, r being Element of REAL d such that A19: A = cell (l,r) and

A20: for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: ( for l, r being Element of REAL d holds

( not A9 = cell (l,r) or ex i being Element of Seg d st

( r . i < l . i implies not [(l . i),(r . i)] is Gap of G . i ) ) or A = A9 )

given l9, r9 being Element of REAL d such that A21: A9 = cell (l9,r9) and

A22: for i being Element of Seg d holds

( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ; :: thesis: A = A9

reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def3;

A23: now :: thesis: for i being Element of Seg d holds

( l . i = l9 . i & r . i = r9 . i )

then
l = l9
by FUNCT_2:63;( l . i = l9 . i & r . i = r9 . i )

let i be Element of Seg d; :: thesis: ( l . i = l9 . i & r . i = r9 . i )

A24: r . i < l . i by A20;

A25: [(l . i),(r . i)] is Gap of G . i by A20;

A26: r9 . i < l9 . i by A22;

[(l9 . i),(r9 . i)] is Gap of G . i by A22;

hence ( l . i = l9 . i & r . i = r9 . i ) by A24, A25, A26, Th19; :: thesis: verum

end;A24: r . i < l . i by A20;

A25: [(l . i),(r . i)] is Gap of G . i by A20;

A26: r9 . i < l9 . i by A22;

[(l9 . i),(r9 . i)] is Gap of G . i by A22;

hence ( l . i = l9 . i & r . i = r9 . i ) by A24, A25, A26, Th19; :: thesis: verum

hence A = A9 by A19, A21, A23, FUNCT_2:63; :: thesis: verum