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

proof

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

end;

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