let k, k9 be Nat; :: thesis: for d being non zero Nat
for l, r, l9, r9 being Element of REAL d
for G being Grating of d st k <= d & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) holds
for i being Element of Seg d holds
( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )
let d be non zero Nat; :: thesis: for l, r, l9, r9 being Element of REAL d
for G being Grating of d st k <= d & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) holds
for i being Element of Seg d holds
( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )
let l, r, l9, r9 be Element of REAL d; :: thesis: for G being Grating of d st k <= d & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) holds
for i being Element of Seg d holds
( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )
let G be Grating of d; :: thesis: ( k <= d & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) implies for i being Element of Seg d holds
( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) )
assume that
A1: k <= d and
A2: k9 <= d and
A3: cell (l,r) in cells (k,G) and
A4: cell (l9,r9) in cells (k9,G) ; :: thesis: ( not cell (l,r) c= cell (l9,r9) or for i being Element of Seg d holds
( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) )
assume A5: cell (l,r) c= cell (l9,r9) ; :: thesis: for i being Element of Seg d holds
( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )
let i be Element of Seg d; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

per cases ( for i being Element of Seg d holds
( ( l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( l9 . i = r9 . i & l9 . i in G . i ) ) or for i being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ) by A2, A4, Th31;

suppose A6: for i being Element of Seg d holds
( ( l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( l9 . i = r9 . i & l9 . i in G . i ) ) ; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

then A7: for i being Element of Seg d holds l9 . i <= r9 . i ;
then A8: l9 . i <= l . i by A5, Th25;
A9: l . i <= r . i by A5, A7, Th25;
A10: r . i <= r9 . i by A5, A7, Th25;
A11: l9 . i <= r . i by A8, A9, XXREAL_0:2;
A12: l . i <= r9 . i by A9, A10, XXREAL_0:2;
thus ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) :: thesis: verum

proof

per cases ( [(l9 . i),(r9 . i)] is Gap of G . i or l9 . i = r9 . i ) by A6;

suppose A13: [(l9 . i),(r9 . i)] is Gap of G . i ; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

A14: now :: thesis: ( l9 . i <> l . i implies not l . i <> r9 . i )

assume that
A15: l9 . i <> l . i and
A16: l . i <> r9 . i ; :: thesis: contradiction
A17: l9 . i < l . i by A8, A15, XXREAL_0:1;
A18: l . i < r9 . i by A12, A16, XXREAL_0:1;
l . i in G . i by A1, A3, Th32;
hence contradiction by A13, A17, A18, Th13; :: thesis: verum

end;

now :: thesis: ( l9 . i <> r . i implies not r . i <> r9 . i )

assume that
A19: l9 . i <> r . i and
A20: r . i <> r9 . i ; :: thesis: contradiction
A21: l9 . i < r . i by A11, A19, XXREAL_0:1;
A22: r . i < r9 . i by A10, A20, XXREAL_0:1;
r . i in G . i by A1, A3, Th32;
hence contradiction by A13, A21, A22, Th13; :: thesis: verum

end;

hence ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) by A9, A14, XXREAL_0:1; :: thesis: verum

end;

suppose l9 . i = r9 . i ; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

hence ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) by A8, A10, A11, A12, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

suppose A23: for i being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

then A24: r9 . i < l9 . i ;
A25: [(l9 . i),(r9 . i)] is Gap of G . i by A23;
thus ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) :: thesis: verum

proof

per cases ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) or for i being Element of Seg d holds
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( l . i = r . i & l . i in G . i ) ) ) by A1, A3, Th31;

suppose A26: for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

then A27: r . i <= r9 . i by A5, Th26;
A28: l9 . i <= l . i by A5, A26, Th26;

A29: now :: thesis: not l9 . i <> l . i

assume l9 . i <> l . i ; :: thesis: contradiction
then A30: l9 . i < l . i by A28, XXREAL_0:1;
l . i in G . i by A1, A3, Th32;
hence contradiction by A24, A25, A30, Th13; :: thesis: verum

end;

now :: thesis: not r . i <> r9 . i

assume r . i <> r9 . i ; :: thesis: contradiction
then A31: r . i < r9 . i by A27, XXREAL_0:1;
r . i in G . i by A1, A3, Th32;
hence contradiction by A24, A25, A31, Th13; :: thesis: verum

end;

hence ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) by A29; :: thesis: verum

end;

suppose A32: for i being Element of Seg d holds
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( l . i = r . i & l . i in G . i ) ) ; :: thesis: ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) )

A33: l . i in G . i by A1, A3, Th32;
r . i in G . i by A1, A3, Th32;
hence ( ( 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 ) or ( l . i <= r . i & r9 . i < l9 . i & r9 . i <= l . i & r . i <= l9 . i ) ) by A24, A25, A32, A33, Th13; :: thesis: verum

end;

end;

end;

end;

end;