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