let n be even Nat; :: thesis: ( not n <= 3 or n = 0 or n = 2 )
assume A1: n <= 3 ; :: thesis: ( n = 0 or n = 2 )
n <> (2 * 1) + 1 ;
then n < 2 + 1 by A1, XXREAL_0:1;
then A2: n <= 2 by NAT_1:13;

per cases ( n = 2 or n < 1 + 1 ) by A2, XXREAL_0:1;

suppose n = 2 ; :: thesis: ( n = 0 or n = 2 )

hence ( n = 0 or n = 2 ) ; :: thesis: verum

end;

suppose n < 1 + 1 ; :: thesis: ( n = 0 or n = 2 )

then n <= 1 by NAT_1:13;
hence ( n = 0 or n = 2 ) by Th10; :: thesis: verum

end;

end;