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 ) ) )
proof
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;
set k = card X;
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
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;
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
( 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;