theorem Th2: :: COMPLEX3:2

for a being Real holds
( ( not a is light & a is negative implies a <= - 1 ) & ( a <= - 1 implies ( not a is light & a is negative ) ) & ( not a is heavy & a is negative implies ( - 1 <= a & a < 0 ) ) & ( - 1 <= a & a < 0 implies ( not a is heavy & a is negative ) ) & ( not a is heavy & a is positive implies ( 0 < a & a <= 1 ) ) & ( 0 < a & a <= 1 implies ( not a is heavy & a is positive ) ) & ( not a is light & a is positive implies 1 <= a ) & ( 1 <= a implies ( not a is light & a is positive ) ) )