Syntax Definition wor 4273

Description: Extend wff notation to include the strict linear ordering predicate. Read: ' 𝑅 orders 𝐴.'

Hypotheses

Ref	Expression
cA	class 𝐴
cR	class 𝑅

Assertion

Ref	Expression
wor	wff 𝑅 Or 𝐴

See definition df-iso 4275 for more information.