|.(a *').| = |.a.| by COMPLEX1:53;
hence not a *' is light by Def2; :: thesis: verum