1 " <= |.a.| " by XREAL_1:85, Def1;
hence not a " is light by COMPLEX1:66; :: thesis: verum