take 4 ; :: thesis: 4 is square-containing
2 |^ 2 = 2 * 2 by NEWTON:81
.= 4 ;
hence 4 is square-containing by INT_2:28; :: thesis: verum