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

let a, b, c be Element of T; :: thesis: Tern ((Tern (a,b,c)),b,a) = Tern (a,b,c)

Tern ((Tern (a,b,c)),b,a) = Tern ((Tern (a,b,c)),b,(Tern (a,b,(b `)))) by TRADef

.= Tern (a,b,(Tern (c,b,(b `)))) by TDis

.= Tern (a,b,c) by TRADef ;

hence Tern ((Tern (a,b,c)),b,a) = Tern (a,b,c) ; :: thesis: verum

let a, b, c be Element of T; :: thesis: Tern ((Tern (a,b,c)),b,a) = Tern (a,b,c)

Tern ((Tern (a,b,c)),b,a) = Tern ((Tern (a,b,c)),b,(Tern (a,b,(b `)))) by TRADef

.= Tern (a,b,(Tern (c,b,(b `)))) by TDis

.= Tern (a,b,c) by TRADef ;

hence Tern ((Tern (a,b,c)),b,a) = Tern (a,b,c) ; :: thesis: verum