|.(- (1 / 2)).| = - (- (1 / 2)) by ABSVALUE:def 1;
then - (1 / 2) is light ;
hence ex b₁ being negative Real st b₁ is light ; :: thesis: verum