Syntax definition wac

Description: Wff for an abbreviation of the axiom of choice.

	Ref	Expression
Assertion	wac	$$wff\mathrm{CHOICE}$$