let a be non heavy Complex; :: thesis: ( a is light or a is weightless )
|.a.| <= 1 by Def1;
hence ( a is light or a is weightless ) by XXREAL_0:1; :: thesis: verum