20 |^ 2 = 20 * 20 by WSIERP_1:1;
hence (20 |^ 2) - 1 = (3 * 7) * 19 ; :: thesis: verum