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

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