set C = the carrier of O;
reconsider g = id the carrier of O as Function of the carrier of O,the carrier of O ;
reconsider g = g as Function of O,O ;
g is dneg by Th20;
hence ex b₁ being Function of O,O st b₁ is dneg ; :: thesis: verum