let n be even perfect_power Nat; :: thesis: 4 divides n
consider x, k being Nat such that
A1: ( k > 1 & n = x |^ k ) by PerPowDef;
2 divides x by INT_2:28, NAT_3:5, A1, ABIAN:def 1;
hence 4 divides n by A1, FourDivPower; :: thesis: verum