let T be Ternary_Boolean_Algebra; for a, b being Element of T holds Tern (a,b,a) = a
let a, b be Element of T; Tern (a,b,a) = a
Tern (a,b,a) =
Tern ((Tern (a,b,(b `))),b,a)
by TRADef
.=
Tern ((Tern (a,b,(b `))),b,(Tern (a,b,(b `))))
by TRADef
.=
Tern (a,b,(Tern ((b `),b,(b `))))
by TDis
.=
Tern (a,b,(b `))
by TLADef
.=
a
by TRADef
;
hence
Tern (a,b,a) = a
; verum