formula_list(usable).

% Huntington's axioms entail Robbins' axioms,...
 
    ( 
	( all x y ( u(c(u(c(x),y)),c(u(c(x),c(y)))) = x )) % BIII
->
	( all x y ( c(u(c(u(x,y)),c(u(x,c(y))))) = x ))    % BIII'
    ).

% ...and vice versa.

    ( 
	( all x y ( c(u(c(u(x,y)),c(u(x,c(y))))) = x ))    % BIII'
->
	( all x y ( u(c(u(c(x),y)),c(u(c(x),c(y)))) = x )) % BIII
    ).

end_of_list.