theorem TA1: :: COMPLEX3:1

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