let e be object ; :: thesis: ( e is natural implies e is integer )
assume A1: e is natural ; :: thesis: e is integer
reconsider e = e as Nat by A1, TARSKI:1;
e is Integer by Th1;
hence e is integer ; :: thesis: verum