take 4 ; :: thesis: 4 is square-containing
2 |^ 2 = 2 * 2 by NEWTON:100
.= 4 ;
hence 4 is square-containing by Def1, INT_2:44; :: thesis: verum