let d be non zero Element of NAT ; :: thesis:
let l, r, l', r' be Element of REAL d; :: thesis:
let G be Grating of d; :: thesis:
let X, X' be Subset of (Seg d); :: thesis:
assume A1: cell l,r c= cell l',r' ; :: thesis:
assume A2: for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ; :: thesis:
assume A3: for i being Element of Seg d holds
( ( i in X' & l' . i < r' . i & [(l' . i),(r' . i)] is Gap of G . i ) or ( not i in X' & l' . i = r' . i & l' . i in G . i ) ) ; :: thesis:
A4: ( l in cell l,r & r in cell l,r ) by Th27;
A5: for i being Element of Seg d holds l' . i <= r' . i by A3;
thus X c= X' :: thesis:

let i be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: ( i in X & not i in X' ) ; :: thesis:
then reconsider i = i as Element of Seg d ;
( l . i < r . i & l' . i = r' . i & l' . i <= l . i & r . i <= r' . i ) by A1, A2, A3, A4, A5, A6, Th25;
hence contradiction by XXREAL_0:2; :: thesis:

end;

set k = card X;
set k' = card X';
card (Seg d) = d by FINSEQ_1:78;
then A7: ( card X <= d & card X' <= d ) by NAT_1:44;
then A8: ( cell l,r in cells (card X),G & cell l',r' in cells (card X'),G ) by A2, A3, Th34;
thus for i being Element of Seg d st ( i in X or not i in X' ) holds
( l . i = l' . i & r . i = r' . i ) :: thesis:

let i be Element of Seg d; :: thesis:
assume A9: ( i in X or not i in X' ) ; :: thesis:
l' . i <= r' . i by A3;
then ( ( l . i = l' . i & r . i = r' . i ) or ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) ) by A1, A7, A8, Th46;
hence ( l . i = l' . i & r . i = r' . i ) by A2, A3, A9; :: thesis:

end;

thus for i being Element of Seg d st not i in X & i in X' & not ( l . i = l' . i & r . i = l' . i ) holds
( l . i = r' . i & r . i = r' . i ) :: thesis:

let i be Element of Seg d; :: thesis:
assume ( not i in X & i in X' ) ; :: thesis:
then ( l . i = r . i & l' . i < r' . i ) by A2, A3;
hence ( ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) ) by A1, A7, A8, Th46; :: thesis:

end;