theorem :: COMPLEX3:81

for a being positive light Real holds
( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 )