reconsider k = 2 -root a as Integer ;
reconsider l = k / 2 as Integer ;
a = (2 * l) * (2 * l)
.= (2 * 2) * (l * l) ;
hence ( a / 4 is square & a / 4 is integer ) ; :: thesis: verum