set Q = LexOrder (I,R);
let a, b be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: ( not a in field (LexOrder (I,R)) or not b in field (LexOrder (I,R)) or not [a,b] in LexOrder (I,R) or not [b,a] in LexOrder (I,R) )
assume ( a in field (LexOrder (I,R)) & b in field (LexOrder (I,R)) ) ; :: thesis: ( not [a,b] in LexOrder (I,R) or not [b,a] in LexOrder (I,R) )
assume A1: ( [a,b] in LexOrder (I,R) & [b,a] in LexOrder (I,R) ) ; :: thesis: contradiction
then reconsider a = a, b = b as Element of I * by ZFMISC_1:87;
set c = a;

per cases ( ( a c< b & b c< a ) or ( a c< b & ex k being Nat st
( k in dom b & k in dom a & [(b . k),(a . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = a . n ) ) ) or ( b c< a & 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 a & [(b . k),(a . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = a . n ) ) ) ) by A1, LO;

suppose ( a c< b & b c< a ) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose A2: ( a c< b & ex k being Nat st
( k in dom b & k in dom a & [(b . k),(a . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = a . n ) ) ) ; :: thesis: contradiction

then consider k being Nat such that
A3: ( k in dom b & k in dom a & [(b . k),(a . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = a . n ) ) ;
[(a . k),(a . k)] in R by A2, A3, Lem12;
hence contradiction by PREFER_1:22; :: thesis: verum

end;

suppose A12: ( b c< a & 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: contradiction

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 ) ) ;
( k in dom a & [(a . k),(a . k)] in R ) by A12, A11, Lem12;
hence contradiction by PREFER_1:22; :: 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 a & [(b . k),(a . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b . n = a . n ) ) ) ; :: thesis: contradiction

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 a & [(b . k2),(a . k2)] in R & ( for n being Nat st 1 <= n & n < k2 holds
b . n = a . n ) ) by A15;

per cases ( k1 < k2 or k1 = k2 or k1 > k2 ) by XXREAL_0:1;

suppose A18: k1 < k2 ; :: thesis: contradiction

k2 <= len a by A17, FINSEQ_3:25;
then ( 1 <= k1 & k1 < len a ) by A16, A18, FINSEQ_3:25, XXREAL_0:2;
then ( k1 in dom a & [(a . k1),(a . k1)] in R ) by A16, A17, A18;
hence contradiction by PREFER_1:22; :: thesis: verum

end;

suppose k1 = k2 ; :: thesis: contradiction

hence contradiction by A16, A17, PREFER_1:22; :: thesis: verum

end;

suppose A22: k1 > k2 ; :: thesis: contradiction

k1 <= len a by A16, FINSEQ_3:25;
then ( 1 <= k2 & k2 < len a ) by A17, A22, FINSEQ_3:25, XXREAL_0:2;
then ( k2 in dom a & [(a . k2),(a . k2)] in R ) by A16, A17, A22;
hence contradiction by PREFER_1:22; :: thesis: verum

end;

end;

end;

end;