let T be Ternary_Boolean_Algebra; 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; (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)
; verum