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