let t be Integer; :: thesis: ( t < 1 iff t <= 0 )
thus ( t < 1 implies t <= 0 ) :: thesis: ( t <= 0 implies t < 1 )

proof

assume A1: t < 1 ; :: thesis: t <= 0
assume A2: t > 0 ; :: thesis: contradiction
then reconsider t = t as Element of NAT by INT_1:3;
t >= 1 by A2, NAT_1:14;
hence contradiction by A1; :: thesis: verum

end;

thus ( t <= 0 implies t < 1 ) ; :: thesis: verum