(non_op C) term (Non a) = a by Th62;
then a at f = (non_op C) term ((Non a) at f) by Def60
.= Non ((Non a) at f) by Th59 ;
hence for b₁ being expression of C, an_Adj C st b₁ = a at f holds
b₁ is negative ; :: thesis: verum