let T be Ternary_Boolean_Algebra; :: thesis: for x being Element of T holds JoinTBA (T,x) absorbs MeetTBA (T,x)
let x be Element of T; :: thesis: JoinTBA (T,x) absorbs MeetTBA (T,x)
set ff = JoinTBA (T,x);
set gg = MeetTBA (T,x);
for a, b being Element of the carrier of T holds (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a

proof

let a, b be Element of the carrier of T; :: thesis: (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a
(JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = (JoinTBA (T,x)) . (a,(Tern (a,(x `),b))) by MeetDef
.= Tern (a,x,(Tern (a,(x `),b))) by JoinDef
.= Tern ((Tern (a,x,(x `))),x,(Tern (a,(x `),b))) by TRADef
.= Tern ((Tern (a,(x `),x)),x,(Tern (a,(x `),b))) by Th36a
.= Tern (a,(x `),(Tern (x,x,b))) by TDis
.= Tern (a,(x `),(Tern (x,b,x))) by Th36a
.= Tern (a,(x `),x) by Th32
.= Tern (a,x,(x `)) by Th36a
.= a by TRADef ;
hence (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a ; :: thesis: verum

end;

hence JoinTBA (T,x) absorbs MeetTBA (T,x) by LATTICE2:def 1; :: thesis: verum