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

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