take a = 1 / 2; :: thesis: ( a is light & a is positive & not a is integer )
|.a.| < 1 ;
hence ( a is light & a is positive & not a is integer ) by COMPLEX3:def 2; :: thesis: verum