let d be non zero Nat; :: thesis: for l, r, l9, r9 being Element of REAL d

for G being Grating of d

for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds

( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

let l, r, l9, r9 be Element of REAL d; :: thesis: for G being Grating of d

for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds

( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

let G be Grating of d; :: thesis: for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds

( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

let X, X9 be Subset of (Seg d); :: thesis: ( cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) implies ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

assume A1: cell (l,r) c= cell (l9,r9) ; :: 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) & not ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) or ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

( l . i = r9 . i & r . i = r9 . 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) & not ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) or ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

assume A3: for i being Element of Seg d holds

( ( i in X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ; :: thesis: ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

A4: l in cell (l,r) by Th23;

A5: r in cell (l,r) by Th23;

A6: for i being Element of Seg d holds l9 . i <= r9 . i by A3;

thus X c= X9 :: thesis: ( ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

set k9 = card X9;

A12: card (Seg d) = d by FINSEQ_1:57;

then A13: card X <= d by NAT_1:43;

A14: card X9 <= d by A12, NAT_1:43;

A15: cell (l,r) in cells ((card X),G) by A2, A13, Th30;

A16: cell (l9,r9) in cells ((card X9),G) by A3, A14, Th30;

thus for i being Element of Seg d st ( i in X or not i in X9 ) holds

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

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

( l . i = r9 . i & r . i = r9 . i ) :: thesis: verum

for G being Grating of d

for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds

( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

let l, r, l9, r9 be Element of REAL d; :: thesis: for G being Grating of d

for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds

( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

let G be Grating of d; :: thesis: for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds

( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

let X, X9 be Subset of (Seg d); :: thesis: ( cell (l,r) c= cell (l9,r9) & ( 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) implies ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

assume A1: cell (l,r) c= cell (l9,r9) ; :: 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) & not ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) or ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

( l . i = r9 . i & r . i = r9 . 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 X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) & not ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) or ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

assume A3: for i being Element of Seg d holds

( ( i in X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ; :: thesis: ( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

A4: l in cell (l,r) by Th23;

A5: r in cell (l,r) by Th23;

A6: for i being Element of Seg d holds l9 . i <= r9 . i by A3;

thus X c= X9 :: thesis: ( ( for i being Element of Seg d st ( i in X or not i in X9 ) holds

( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds

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

proof

set k = card X;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in X or i in X9 )

assume that

A7: i in X and

A8: not i in X9 ; :: thesis: contradiction

reconsider i = i as Element of Seg d by A7;

A9: l . i < r . i by A2, A7;

A10: l9 . i = r9 . i by A3, A8;

A11: l9 . i <= l . i by A1, A4, A6, Th21;

r . i <= r9 . i by A1, A5, A6, Th21;

hence contradiction by A9, A10, A11, XXREAL_0:2; :: thesis: verum

end;assume that

A7: i in X and

A8: not i in X9 ; :: thesis: contradiction

reconsider i = i as Element of Seg d by A7;

A9: l . i < r . i by A2, A7;

A10: l9 . i = r9 . i by A3, A8;

A11: l9 . i <= l . i by A1, A4, A6, Th21;

r . i <= r9 . i by A1, A5, A6, Th21;

hence contradiction by A9, A10, A11, XXREAL_0:2; :: thesis: verum

set k9 = card X9;

A12: card (Seg d) = d by FINSEQ_1:57;

then A13: card X <= d by NAT_1:43;

A14: card X9 <= d by A12, NAT_1:43;

A15: cell (l,r) in cells ((card X),G) by A2, A13, Th30;

A16: cell (l9,r9) in cells ((card X9),G) by A3, A14, Th30;

thus for i being Element of Seg d st ( i in X or not i in X9 ) holds

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

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

proof

thus
for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds
let i be Element of Seg d; :: thesis: ( ( i in X or not i in X9 ) implies ( l . i = l9 . i & r . i = r9 . i ) )

assume A17: ( i in X or not i in X9 ) ; :: thesis: ( l . i = l9 . i & r . i = r9 . i )

l9 . i <= r9 . i by A3;

then ( ( l . i = l9 . i & r . i = r9 . i ) or ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A1, A13, A14, A15, A16, Th42;

hence ( l . i = l9 . i & r . i = r9 . i ) by A2, A3, A17; :: thesis: verum

end;assume A17: ( i in X or not i in X9 ) ; :: thesis: ( l . i = l9 . i & r . i = r9 . i )

l9 . i <= r9 . i by A3;

then ( ( l . i = l9 . i & r . i = r9 . i ) or ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A1, A13, A14, A15, A16, Th42;

hence ( l . i = l9 . i & r . i = r9 . i ) by A2, A3, A17; :: thesis: verum

( l . i = r9 . i & r . i = r9 . i ) :: thesis: verum

proof

let i be Element of Seg d; :: thesis: ( not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) implies ( l . i = r9 . i & r . i = r9 . i ) )

assume that

A18: not i in X and

A19: i in X9 ; :: thesis: ( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )

A20: l . i = r . i by A2, A18;

l9 . i < r9 . i by A3, A19;

hence ( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A1, A13, A14, A15, A16, A20, Th42; :: thesis: verum

end;assume that

A18: not i in X and

A19: i in X9 ; :: thesis: ( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )

A20: l . i = r . i by A2, A18;

l9 . i < r9 . i by A3, A19;

hence ( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A1, A13, A14, A15, A16, A20, Th42; :: thesis: verum