(non_op C) term (Non a) = a by Th44b;
then a at f = (non_op C) term ((Non a) at f) by SUBST
.= Non ((Non a) at f) by Th44 ;
hence a at f is negative expression of C, an_Adj C ; :: thesis: verum