let a be Real; :: thesis: 0 <= a ^2
per cases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; :: thesis: 0 <= a ^2
hence 0 <= a ^2 ; :: thesis: verum
end;
suppose a <> 0 ; :: thesis: 0 <= a ^2
hence 0 <= a ^2 by SQUARE_1:12; :: thesis: verum
end;
end;