let j be Nat; :: thesis: ( j < 1 implies j = 0 )
assume j < 1 ; :: thesis: j = 0
then j < 0 + 1 ;
then A1: j <= 0 by Th13;
assume j <> 0 ; :: thesis: contradiction
hence contradiction by A1, Th2; :: thesis: verum