g = - (- g) by Th40;
then ( not - g is zero & - g is nonnegative ) ;
hence - g is positive ; :: thesis: verum