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

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

set b1 = Tern (a,b,c);

set b2 = Tern (a,b,d);

Tern (a,b,(Tern (c,b,d))) = Tern ((Tern (a,b,c)),b,(Tern (a,b,d))) by TDis

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

.= Tern ((Tern (a,b,c)),b,(Tern ((Tern (a,b,c)),b,d))) by Lemma33

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

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

.= Tern ((Tern (a,b,c)),b,d) by TLADef ;

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

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

set b1 = Tern (a,b,c);

set b2 = Tern (a,b,d);

Tern (a,b,(Tern (c,b,d))) = Tern ((Tern (a,b,c)),b,(Tern (a,b,d))) by TDis

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

.= Tern ((Tern (a,b,c)),b,(Tern ((Tern (a,b,c)),b,d))) by Lemma33

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

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

.= Tern ((Tern (a,b,c)),b,d) by TLADef ;

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