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

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:16;
t >= 1 by A2, NAT_1:14;
hence contradiction by A1; :: thesis: verum

end;

hence ( t < 1 iff t <= 0 ) ; :: thesis: verum