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