( b < 1 & 1 + 0 < 1 + b ) by COMPLEX3:1;
then [/b\] = 1 by INT_1:def 7;
hence ( [/b\] is weightless & [/b\] is positive ) ; :: thesis: verum