let T be

Ternary_Boolean_Algebra;

for a, b being Element of T holds Tern ((b `),b,a) = Tern (a,b,(b `))let a,

b be

Element of

T;

Tern ((b `),b,a) = Tern (a,b,(b `))
Tern (

(b `),

b,

a)

= a
by TLADef;

hence
Tern (

(b `),

b,

a)

= Tern (

a,

b,

(b `))

by TRADef;

verum