let a be Real; :: thesis: 0 <= a * a
per cases ( 0 <= a or not 0 <= a ) ;
suppose 0 <= a ; :: thesis: 0 <= a * a
hence 0 <= a * a ; :: thesis: verum
end;
suppose not 0 <= a ; :: thesis: 0 <= a * a
hence 0 <= a * a ; :: thesis: verum
end;
end;