set Q = LexOrder (I,R);
let a, b, c be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not a in field (LexOrder (I,R)) or not b in field (LexOrder (I,R)) or not c in field (LexOrder (I,R)) or not [a,b] in LexOrder (I,R) or not [b,c] in LexOrder (I,R) or [a,c] in LexOrder (I,R) )
assume ( a in field (LexOrder (I,R)) & b in field (LexOrder (I,R)) & c in field (LexOrder (I,R)) ) ; :: thesis: ( not [a,b] in LexOrder (I,R) or not [b,c] in LexOrder (I,R) or [a,c] in LexOrder (I,R) )
assume A1: ( [a,b] in LexOrder (I,R) & [b,c] in LexOrder (I,R) ) ; :: thesis: [a,c] in LexOrder (I,R)
then reconsider a = a, b = b, c = c as Element of I * by ZFMISC_1:87;
per cases ( ( a c< b & b c< c ) or ( a c< b & ex k being Nat st
( k in dom b & k in dom c & [(b . k),(c . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = c . n ) ) ) or ( b c< c & ex k being Nat st
( k in dom a & k in dom b & [(a . k),(b . k)] in R & ( for n being Nat st 1 <= n & n < k holds
a . n = b . n ) ) ) or ( ex k being Nat st
( k in dom a & k in dom b & [(a . k),(b . k)] in R & ( for n being Nat st 1 <= n & n < k holds
a . n = b . n ) ) & ex k being Nat st
( k in dom b & k in dom c & [(b . k),(c . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = c . n ) ) ) ) by A1, LO;
suppose ( a c< b & b c< c ) ; :: thesis: [a,c] in LexOrder (I,R)
then a c< c by XBOOLE_1:56;
hence [a,c] in LexOrder (I,R) by LO; :: thesis: verum
end;
suppose A2: ( a c< b & ex k being Nat st
( k in dom b & k in dom c & [(b . k),(c . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = c . n ) ) ) ; :: thesis: [a,c] in LexOrder (I,R)
then consider k being Nat such that
A3: ( k in dom b & k in dom c & [(b . k),(c . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = c . n ) ) ;
per cases ( len a < k or len a >= k ) ;
suppose A4: len a < k ; :: thesis: [a,c] in LexOrder (I,R)
k <= len c by A3, FINSEQ_3:25;
then A5: len a < len c by A4, XXREAL_0:2;
for n being Nat st n in dom a holds
a . n = c . n
proof
let n be Nat; :: thesis: ( n in dom a implies a . n = c . n )
assume A6: n in dom a ; :: thesis: a . n = c . n
then n <= len a by FINSEQ_3:25;
then ( 1 <= n & n < k ) by A4, A6, XXREAL_0:2, FINSEQ_3:25;
then b . n = c . n by A3;
hence a . n = c . n by A2, A6, Lem12; :: thesis: verum
end;
then a c< c by A5, Lem12;
hence [a,c] in LexOrder (I,R) by LO; :: thesis: verum
end;
suppose A7: len a >= k ; :: thesis: [a,c] in LexOrder (I,R)
1 <= k by A3, FINSEQ_3:25;
then A8: k in dom a by A7, FINSEQ_3:25;
then A9: [(a . k),(c . k)] in R by A2, A3, Lem12;
for n being Nat st 1 <= n & n < k holds
a . n = c . n
proof
let n be Nat; :: thesis: ( 1 <= n & n < k implies a . n = c . n )
assume A10: ( 1 <= n & n < k ) ; :: thesis: a . n = c . n
then n < len a by A7, XXREAL_0:2;
then n in dom a by A10, FINSEQ_3:25;
then a . n = b . n by A2, Lem12;
hence a . n = c . n by A10, A3; :: thesis: verum
end;
hence [a,c] in LexOrder (I,R) by A3, A8, A9, LO; :: thesis: verum
end;
end;
end;
suppose A12: ( b c< c & ex k being Nat st
( k in dom a & k in dom b & [(a . k),(b . k)] in R & ( for n being Nat st 1 <= n & n < k holds
a . n = b . n ) ) ) ; :: thesis: [a,c] in LexOrder (I,R)
then consider k being Nat such that
A11: ( k in dom a & k in dom b & [(a . k),(b . k)] in R & ( for n being Nat st 1 <= n & n < k holds
a . n = b . n ) ) ;
dom b c= dom c by A12, XBOOLE_0:def 8, XTUPLE_0:8;
then A13: ( k in dom c & [(a . k),(c . k)] in R ) by A12, A11, Lem12;
for n being Nat st 1 <= n & n < k holds
a . n = c . n
proof
let n be Nat; :: thesis: ( 1 <= n & n < k implies a . n = c . n )
assume A14: ( 1 <= n & n < k ) ; :: thesis: a . n = c . n
k <= len b by A11, FINSEQ_3:25;
then n < len b by A14, XXREAL_0:2;
then b . n = c . n by A12, Lem12, A14, FINSEQ_3:25;
hence a . n = c . n by A11, A14; :: thesis: verum
end;
hence [a,c] in LexOrder (I,R) by A11, A13, LO; :: thesis: verum
end;
suppose A15: ( ex k being Nat st
( k in dom a & k in dom b & [(a . k),(b . k)] in R & ( for n being Nat st 1 <= n & n < k holds
a . n = b . n ) ) & ex k being Nat st
( k in dom b & k in dom c & [(b . k),(c . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = c . n ) ) ) ; :: thesis: [a,c] in LexOrder (I,R)
then consider k1 being Nat such that
A16: ( k1 in dom a & k1 in dom b & [(a . k1),(b . k1)] in R & ( for n being Nat st 1 <= n & n < k1 holds
a . n = b . n ) ) ;
consider k2 being Nat such that
A17: ( k2 in dom b & k2 in dom c & [(b . k2),(c . k2)] in R & ( for n being Nat st 1 <= n & n < k2 holds
b . n = c . n ) ) by A15;
per cases ( k1 < k2 or k1 = k2 or k1 > k2 ) by XXREAL_0:1;
suppose A18: k1 < k2 ; :: thesis: [a,c] in LexOrder (I,R)
k2 <= len c by A17, FINSEQ_3:25;
then ( 1 <= k1 & k1 < len c ) by A16, A18, FINSEQ_3:25, XXREAL_0:2;
then A19: ( k1 in dom c & [(a . k1),(c . k1)] in R ) by A16, A17, A18, FINSEQ_3:25;
for n being Nat st 1 <= n & n < k1 holds
a . n = c . n
proof
let n be Nat; :: thesis: ( 1 <= n & n < k1 implies a . n = c . n )
assume ( 1 <= n & n < k1 ) ; :: thesis: a . n = c . n
then ( a . n = b . n & 1 <= n & n < k2 ) by A16, A18, XXREAL_0:2;
hence a . n = c . n by A17; :: thesis: verum
end;
hence [a,c] in LexOrder (I,R) by A16, A19, LO; :: thesis: verum
end;
suppose A20: k1 = k2 ; :: thesis: [a,c] in LexOrder (I,R)
then A21: [(a . k1),(c . k1)] in R by A16, A17, RELAT_2:31;
for n being Nat st 1 <= n & n < k1 holds
a . n = c . n
proof
let n be Nat; :: thesis: ( 1 <= n & n < k1 implies a . n = c . n )
assume ( 1 <= n & n < k1 ) ; :: thesis: a . n = c . n
then ( a . n = b . n & b . n = c . n ) by A16, A17, A20;
hence a . n = c . n ; :: thesis: verum
end;
hence [a,c] in LexOrder (I,R) by A20, A16, A17, A21, LO; :: thesis: verum
end;
suppose A22: k1 > k2 ; :: thesis: [a,c] in LexOrder (I,R)
k1 <= len a by A16, FINSEQ_3:25;
then ( 1 <= k2 & k2 < len a ) by A17, A22, FINSEQ_3:25, XXREAL_0:2;
then A19: ( k2 in dom a & [(a . k2),(c . k2)] in R ) by A16, A17, A22, FINSEQ_3:25;
for n being Nat st 1 <= n & n < k2 holds
a . n = c . n
proof
let n be Nat; :: thesis: ( 1 <= n & n < k2 implies a . n = c . n )
assume ( 1 <= n & n < k2 ) ; :: thesis: a . n = c . n
then ( c . n = b . n & 1 <= n & n < k1 ) by A17, A22, XXREAL_0:2;
hence a . n = c . n by A16; :: thesis: verum
end;
hence [a,c] in LexOrder (I,R) by A17, A19, LO; :: thesis: verum
end;
end;
end;
end;