let A, A9 be Cell of d,G; ( 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 )
; ( 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 )
; A = A9
reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def3;
then
l = l9
by FUNCT_2:63;
hence
A = A9
by A19, A21, A23, FUNCT_2:63; verum