let a be Integer; :: thesis: a * a is not Prime
reconsider b = |.a.| as Element of NAT ;
A1: a * a = a ^2
.= |.a.| ^2 by COMPLEX1:75
.= b * b ;

per cases ( b < 2 or 2 <= b ) ;

suppose b < 2 ; :: thesis: a * a is not Prime

then ( b = 0 or b = 1 ) by NAT_1:23;
hence a * a is not Prime by A1, INT_2:def 4; :: thesis: verum

end;

suppose 2 <= b ; :: thesis: a * a is not Prime

then 1 < b by XXREAL_0:2;
then A2: b * 1 < b * b by XREAL_1:68;
b divides b * b by INT_1:def 3;
hence a * a is not Prime by A1, A2, INT_2:def 4; :: thesis: verum

end;

end;