let n be non zero Nat; :: thesis:
given X, Y being Subset of () such that A1: X <> {} and
A2: Y <> {} and
A3: [#] () = X \/ Y and
A4: X misses Y and
A5: the InternalRel of () = ( the InternalRel of () |_2 X) \/ ( the InternalRel of () |_2 Y) ; :: according to ORDERS_3:def 2,ORDERS_3:def 3 :: thesis: contradiction
A6: ( the carrier of () = n & 0 in n ) by ;
per cases ( 0 in X or 0 in Y ) by ;
suppose A7: 0 in X ; :: thesis: contradiction
defpred S1[ Nat] means \$1 in Y;
consider x being Element of () such that
A8: x in Y by ;
x in the carrier of () ;
then x in Segm n by Th19;
then x is natural ;
then A9: ex x being Nat st S1[x] by A8;
consider k being Nat such that
A10: S1[k] and
A11: for i being Nat st S1[i] holds
k <= i from k <> 0 by ;
then consider i being Nat such that
A12: k = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A13: not i in Y by ;
A14: not i + 1 in X by ;
A15: [i,(i + 1)] in the InternalRel of () by ;
now :: thesis: contradiction
per cases ( [i,(i + 1)] in the InternalRel of () |_2 X or [i,(i + 1)] in the InternalRel of () |_2 Y ) by ;
suppose [i,(i + 1)] in the InternalRel of () |_2 X ; :: thesis: contradiction
end;
suppose [i,(i + 1)] in the InternalRel of () |_2 Y ; :: thesis: contradiction
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A16: 0 in Y ; :: thesis: contradiction
defpred S1[ Nat] means \$1 in X;
consider y being Element of () such that
A17: y in X by ;
y in the carrier of () ;
then y in Segm n by Th19;
then y is natural ;
then A18: ex y being Nat st S1[y] by A17;
consider k being Nat such that
A19: S1[k] and
A20: for i being Nat st S1[i] holds
k <= i from k <> 0 by ;
then consider i being Nat such that
A21: k = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A22: not i in X by ;
A23: not i + 1 in Y by ;
A24: [i,(i + 1)] in the InternalRel of () by ;
now :: thesis: contradiction
per cases ( [i,(i + 1)] in the InternalRel of () |_2 Y or [i,(i + 1)] in the InternalRel of () |_2 X ) by ;
suppose [i,(i + 1)] in the InternalRel of () |_2 Y ; :: thesis: contradiction
end;
suppose [i,(i + 1)] in the InternalRel of () |_2 X ; :: thesis: contradiction
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;