let T be Ternary_Boolean_Algebra; :: thesis: for a, b being Element of T holds Tern (a,b,a) = a

let a, b be Element of T; :: thesis: 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 ; :: thesis: verum

let a, b be Element of T; :: thesis: 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 ; :: thesis: verum