let a be Nat; :: thesis: seq (a,0) = {}
hereby :: thesis: verum
set x = the Element of seq (a,0);
assume A1: seq (a,0) <> {} ; :: thesis: contradiction
then reconsider x = the Element of seq (a,0) as Element of NAT by TARSKI:def 3;
( 1 + a <= x & x <= 0 + a ) by A1, Th1;
hence contradiction by NAT_1:13; :: thesis: verum
end;