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