let n be Nat; :: thesis: ( not n <= 7 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 )
assume n <= 7 ; :: thesis: ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 )
then n <= 6 + 1 ;
hence ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 ) by Th8, Th31; :: thesis: verum