let n be Nat; :: thesis: ( not n < 5 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )
assume n < 5 ; :: thesis: ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )
then n < 4 + 1 ;
then n <= 4 by NAT_1:13;
then not not n = 0 & ... & not n = 4 ;
hence ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 ) ; :: thesis: verum