let a be even Integer; :: thesis: ( not 4 divides a implies not a is square )
assume A1: not 4 divides a ; :: thesis: not a is square
not 2 divides a / 2

proof

assume 2 divides a / 2 ; :: thesis: contradiction
then 2 * 2 divides (a / 2) * 2 by NEWTON02:2;
hence contradiction by A1; :: thesis: verum

end;

then reconsider b = a / 2 as odd Integer by ABIAN:def 1;
not 2 * b is square ;
hence not a is square ; :: thesis: verum