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

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in X or i in X' )
assume that
A7: i in X and
A8: not i in X' ; :: thesis: contradiction
reconsider i = i as Element of Seg d by A7;
A9: l . i < r . i by A2, A7;
A10: l' . i = r' . i by A3, A8;
A11: l' . i <= l . i by A1, A4, A6, Th25;
r . i <= r' . i by A1, A5, A6, Th25;
hence contradiction by A9, A10, A11, XXREAL_0:2; :: thesis: verum

end;

set k = card X;
set k' = card X';
A12: card (Seg d) = d by FINSEQ_1:78;
then A13: card X <= d by NAT_1:44;
A14: card X' <= d by A12, NAT_1:44;
A15: cell l,r in cells (card X),G by A2, A13, Th34;
A16: cell l',r' in cells (card X'),G by A3, A14, 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: 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 )

proof

let i be Element of Seg d; :: thesis: ( ( i in X or not i in X' ) implies ( l . i = l' . i & r . i = r' . i ) )
assume A17: ( i in X or not i in X' ) ; :: thesis: ( l . i = l' . i & r . i = r' . i )
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, A13, A14, A15, A16, Th46;
hence ( l . i = l' . i & r . i = r' . i ) by A2, A3, A17; :: thesis: verum

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: verum

proof

let i be Element of Seg d; :: thesis: ( not i in X & i in X' & not ( l . i = l' . i & r . i = l' . i ) implies ( l . i = r' . i & r . i = r' . i ) )
assume that
A18: not i in X and
A19: i in X' ; :: thesis: ( ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) )
A20: l . i = r . i by A2, A18;
l' . i < r' . i by A3, A19;
hence ( ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) ) by A1, A13, A14, A15, A16, A20, Th46; :: thesis: verum

end;