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

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