let T be Ternary_Boolean_Algebra; :: thesis: for a, b, c being Element of T holds Tern (a,b,c) = Tern (a,c,b)
let a, b, c be Element of T; :: thesis: Tern (a,b,c) = Tern (a,c,b)
Tern (a,b,c) = Tern (a,b,(Tern (a,c,(a `)))) by Th35
.= Tern ((Tern (a,b,a)),c,(Tern (a,b,(a `)))) by TDis
.= Tern (a,c,(Tern (a,b,(a `)))) by Th32
.= Tern (a,c,b) by Th35 ;
hence Tern (a,b,c) = Tern (a,c,b) ; :: thesis: verum