let T be Ternary_Boolean_Algebra; for x being Element of T holds JoinTBA (T,x) absorbs MeetTBA (T,x)
let x be Element of T; 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;
(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
;
verum
end;
hence
JoinTBA (T,x) absorbs MeetTBA (T,x)
by LATTICE2:def 1; verum