g = - (- g) by Th40;
hence - g is nonpositive by Def16; :: thesis: verum