|.(a ").| = |.a.| " by COMPLEX1:66;
hence a " is light by XREAL_1:212, Def1; :: thesis: verum