|.a.| * |.b.| > 1 by TA1;
hence a * b is heavy by COMPLEX1:65; :: thesis: verum