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