( |.a.| >= 1 & |.b.| >= 1 ) by Def2;
then |.a.| * |.b.| >= 1 by XREAL_1:159;
hence not a * b is light by COMPLEX1:65; :: thesis: verum