Syntax definition wtr

Description: Extend wff notation to include transitive classes. Notation from TakeutiZaring p. 35.

	Ref	Expression
Assertion	wtr	$$wff\mathrm{Tr}A$$