|.(a ").| = |.a.| " by COMPLEX1:66;
hence not a " is heavy by XREAL_1:211, Def2; :: thesis: verum