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

per cases ( 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 ) ) or for i being Element of Seg d holds
( r' . i < l' . i & [(l' . i),(r' . i)] is Gap of G . i ) ) by A2, A4, Th35;

suppose A6: 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 = l' . i & r . i = r' . i ) or ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) or ( l . i <= r . i & r' . i < l' . i & r' . i <= l . i & r . i <= l' . i ) )

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

proof

per cases ( [(l' . i),(r' . i)] is Gap of G . i or l' . i = r' . i ) by A6;

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

A14: now

assume that
A15: l' . i <> l . i and
A16: l . i <> r' . i ; :: thesis: contradiction
A17: l' . i < l . i by A8, A15, XXREAL_0:1;
A18: l . i < r' . i by A12, A16, XXREAL_0:1;
l . i in G . i by A1, A3, Th36;
hence contradiction by A13, A17, A18, Th17; :: thesis: verum

end;

now

assume that
A19: l' . i <> r . i and
A20: r . i <> r' . i ; :: thesis: contradiction
A21: l' . i < r . i by A11, A19, XXREAL_0:1;
A22: r . i < r' . i by A10, A20, XXREAL_0:1;
r . i in G . i by A1, A3, Th36;
hence contradiction by A13, A21, A22, Th17; :: thesis: verum

end;

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

end;

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

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

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

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 = l' . i & r . i = r' . i ) or ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) or ( l . i <= r . i & r' . i < l' . i & r' . i <= l . i & r . i <= l' . i ) )

then A27: r . i <= r' . i by A5, Th30;
A28: l' . i <= l . i by A5, A26, Th30;

A29: now

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

end;

now

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

end;

hence ( ( 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 ) or ( l . i <= r . i & r' . i < l' . i & r' . i <= l . i & r . i <= l' . 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 = l' . i & r . i = r' . i ) or ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) or ( l . i <= r . i & r' . i < l' . i & r' . i <= l . i & r . i <= l' . i ) )

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

end;

end;

end;

end;

end;