let i be Integer; :: thesis: ( not i is even implies not i is empty )

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: ( not i is even implies not i is empty )

then i in NAT by INT_1:16;
hence ( not i is even implies not i is empty ) by Th12; :: thesis: verum

end;

suppose i < 0 ; :: thesis: ( not i is even implies not i is empty )

hence ( not i is even implies not i is empty ) ; :: thesis: verum

end;

end;