let n be Nat; :: thesis: ( n = 0 or 1 <= n )
( n = 0 or 0 < 0 + n ) ;
hence ( n = 0 or 1 <= n ) by NAT_1:19; :: thesis: verum