let a be Real; :: thesis: 0 <= a * a
( 0 <= a or a < 0 ) ;
hence 0 <= a * a ; :: thesis: verum