let n be Nat; :: thesis: ( not n <= 2 or n = 0 or n = 1 or n = 2 )
assume n <= 2 ; :: thesis: ( n = 0 or n = 1 or n = 2 )
then n <= 1 + 1 ;
hence ( n = 0 or n = 1 or n = 2 ) by Th8, Th26; :: thesis: verum