let A, A' 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
( 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 ) ) ) implies A = A' )
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 A' = 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 = A' )
given l', r' being Element of REAL d such that A21: A' = cell l',r' and
A22: for i being Element of Seg d holds
( r' . i < l' . i & [(l' . i),(r' . i)] is Gap of G . i ) ; :: thesis: A = A'
reconsider l = l, r = r, l' = l', r' = r' as Function of Seg d, REAL by Def4;

A23: now

let i be Element of Seg d; :: thesis: ( l . i = l' . i & r . i = r' . i )
A24: r . i < l . i by A20;
A25: [(l . i),(r . i)] is Gap of G . i by A20;
A26: r' . i < l' . i by A22;
[(l' . i),(r' . i)] is Gap of G . i by A22;
hence ( l . i = l' . i & r . i = r' . i ) by A24, A25, A26, Th23; :: thesis: verum

end;

then l = l' by FUNCT_2:113;
hence A = A' by A19, A21, A23, FUNCT_2:113; :: thesis: verum