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

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

hence
MeetTBA (T,x) absorbs JoinTBA (T,x)
by LATTICE2:def 1; :: thesis: verum
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;(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