Syntax Definition wn 4

Description: If a is a term, so is a^⊥.

Hypothesis

Ref	Expression
wva	term  a

Assertion

Ref	Expression
wn	term  a⊥

This syntax is primitive. The first axiom using it is ax-a1 30.