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 involutive ;
hence ex b₁ being Function of O,O st b₁ is involutive ; :: thesis: verum