let T be Ternary_Boolean_Algebra; :: thesis: for a, b, c, x being Element of T holds Tern (a,b,c) = Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c)))),(x `),(Tern (c,x,a)))
let a, b, c, x be Element of T; :: thesis: Tern (a,b,c) = Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c)))),(x `),(Tern (c,x,a)))
W1: Tern (a,x,(x `)) = a by TRADef;
W2: Tern ((x `),x,b) = b by TLADef;
K1: Tern (a,b,x) = Tern (a,x,b) by Th36a;
K2: Tern (a,b,(x `)) = Tern (a,(x `),b) by Th36a;
POM1: Tern (a,x,b) = Tern (b,x,a) by Th36c;
POM2: Tern ((x `),x,b) = Tern (b,x,(x `)) by Th36c;
POM3: Tern ((Tern (b,x,a)),c,(Tern (b,x,(x `)))) = Tern (b,x,(Tern (a,c,(x `)))) by TDis;
POM4: Tern (b,x,(Tern (a,c,(x `)))) = Tern ((Tern (a,c,(x `))),x,b) by Th36c;
POM5: Tern (b,c,(x `)) = Tern (b,(x `),c) by Th36a;
Tern (a,b,c) = Tern (a,b,(Tern (x,c,(x `)))) by Th35
.= Tern ((Tern (a,b,x)),c,(Tern (a,b,(x `)))) by TDis
.= Tern ((Tern ((Tern (a,x,b)),c,(Tern (a,x,(x `))))),(x `),(Tern ((Tern (a,x,b)),c,(Tern ((x `),x,b))))) by TDis, W1, W2, K1, K2
.= Tern ((Tern (a,x,(Tern (b,c,(x `))))),(x `),(Tern ((Tern (a,c,(x `))),x,b))) by POM1, POM2, POM3, POM4, TDis
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern ((Tern (a,c,(x `))),x,b))) by POM5, TDis
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern (x,b,(Tern (a,c,(x `)))))) by Th36b
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern (x,b,(Tern (a,(x `),c))))) by Th36a
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern ((Tern (x,b,a)),(x `),(Tern (x,b,c))))) by TDis
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern ((Tern (a,b,x)),(x `),(Tern (x,b,c))))) by Th36c
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern ((Tern (a,b,x)),(x `),(Tern (c,b,x))))) by Th36c
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern ((Tern (a,x,b)),(x `),(Tern (c,b,x))))) by Th36a
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (a,x,c)))),(x `),(Tern ((Tern (a,x,b)),(x `),(Tern (c,x,b))))) by Th36a
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (c,x,a)))),(x `),(Tern ((Tern (a,x,b)),(x `),(Tern (c,x,b))))) by Th36c
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (c,x,a)))),(x `),(Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c))))) by Th36c
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c)))),(x `),(Tern ((Tern (a,x,b)),(x `),(Tern (c,x,a))))) by Th36c
.= Tern ((Tern (a,x,b)),(x `),(Tern ((Tern (b,x,c)),(x `),(Tern (c,x,a))))) by TDis
.= Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c)))),(x `),(Tern (c,x,a))) by Th33 ;
hence Tern (a,b,c) = Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c)))),(x `),(Tern (c,x,a))) ; :: thesis: verum