let j be Element of NAT ; :: thesis: ( j < 1 implies j = 0 )
assume j < 1 ; :: thesis: j = 0
then j < 0 + 1 ;
then A1: j <= 0 by NAT_1:13;
assume j <> 0 ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum