then
not x inlim_sup A1
byA2, KURATO_0:def 5; then consider n2 being Nat such that A7:
for k being Nat holds not x in A1 .(n2 + k)byKURATO_0:5; consider k1 being Nat such that A8:
not x in A2 .((n1 + n2)+ k1)byA6, KURATO_0:4; A9:
( ( x in A1 .(n1 +(n2 + k1)) & not x in A2 .(n1 +(n2 + k1)) ) or ( not x in A1 .(n1 +(n2 + k1)) & x in A2 .(n1 +(n2 + k1)) ) )
byA4;
not x in A1 .(n2 +(n1 + k1))byA7; hence
contradiction
byA8, A9; :: thesis: verum
then consider n3 being Nat such that A11:
for k being Nat holds x in A2 .(n3 + k)byKURATO_0:4; consider n2 being Nat such that A12:
for k being Nat holds x in A1 .(n2 + k)byA10, KURATO_0:4; A13:
( ( x in A1 .(n1 +(n2 + n3)) & not x in A2 .(n1 +(n2 + n3)) ) or ( not x in A1 .(n1 +(n2 + n3)) & x in A2 .(n1 +(n2 + n3)) ) )
byA4; A14:
x in A2 .(n3 +(n1 + n2))byA11;
x in A1 .(n2 +(n1 + n3))byA12; hence
contradiction
byA14, A13; :: thesis: verum