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

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

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

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

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

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

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

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

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

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

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

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

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