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