"f = (f, f+), j = (j, j+), y = (y, y+), and c = (c, c+) Î B1,

[(f Þ j)&(y Þ c)] Þ [(f*y) Þ (j*c)];

(f Û j) Þ [(f*y Û j*y)];

(fWj) Þ [(f*y)W(j*y)];

Two-fold universal instantiation:

Operator instantiation: * as a universal operator can be bound to &, Å, &-, Å, Ä, Æ, Ä-, Æ-. (f Þ j) is designated (bipolar true (−1, +1)); ((f, f+)*(y, y+)) is undesignated.

Variable instantiation:

"x, (f, f+)(x) Þ (j, j+)(x); (f, f+)(A); \ (j, j+) (A).