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