let T be Ternary_Boolean_Algebra; :: thesis: for x, a, b, c being Element of T holds (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c)))
let x, a, b, c be Element of T; :: thesis: (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c)))
set ff = JoinTBA (T,x);
(JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . ((Tern (a,x,b)),c) by JoinDef
.= Tern ((Tern (a,x,b)),x,c) by JoinDef
.= Tern (a,x,(Tern (b,x,c))) by Th33
.= Tern (a,x,((JoinTBA (T,x)) . (b,c))) by JoinDef
.= (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c))) by JoinDef ;
hence (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c))) ; :: thesis: verum