Syntax definition w-bnj19

Description: Extend wff notation with the following predicate: B is transitive for A and R . (New usage is discouraged.)

	Ref	Expression
Assertion	w-bnj19	wff _TrFo ( B , A , R )