let n be even Nat; :: thesis: ( n <= 1 implies n = 0 )
assume A1: n <= 1 ; :: thesis: n = 0
n <> (2 * 0 ) + 1 ;
then n < 0 + 1 by A1, XXREAL_0:1;
then ( n <= 0 & n >= 0 ) by NAT_1:13;
hence n = 0 ; :: thesis: verum