Arg (0. (TOP-REAL 2)) = 0 by Th17, COMPTRIG:35;