let i be natural Number ; :: thesis: ( i < 1 implies i = 0 )
assume i < 1 ; :: thesis: i = 0
then i < 0 + 1 ;
then i <= 0 by Th13;
hence i = 0 by Th2; :: thesis: verum