set T = BA2TBA B;
set ff = RosTrn B;
t1:
for a, b being Element of (BA2TBA B) holds Tern (b,b,a) = b
proof
let a,
b be
Element of
(BA2TBA B);
Tern (b,b,a) = b
reconsider aa =
a,
bb =
b as
Element of
B ;
Tern (
b,
b,
a) =
Ros (
bb,
bb,
aa)
by RosTrnDef
.=
bb "\/" ((aa "/\" bb) "\/" (aa "/\" bb))
by LATTICES:def 5
.=
b
by LATTICES:def 8
;
hence
Tern (
b,
b,
a)
= b
;
verum
end;
T4:
for a, b being Element of (BA2TBA B) holds Tern (a,b,b) = b
proof
let a,
b be
Element of
(BA2TBA B);
Tern (a,b,b) = b
reconsider aa =
a,
bb =
b as
Element of
B ;
Tern (
a,
b,
b) =
Ros (
aa,
bb,
bb)
by RosTrnDef
.=
bb "\/" (bb "/\" aa)
by LATTICES:def 8
.=
bb
by LATTICES:def 8
;
hence
Tern (
a,
b,
b)
= b
;
verum
end;
T5:
for a, b being Element of (BA2TBA B) holds Tern ((b `),b,a) = a
proof
let a,
b be
Element of
(BA2TBA B);
Tern ((b `),b,a) = a
reconsider aa =
a,
bb =
b as
Element of
B ;
b ` = bb `
by TBACompl;
then Tern (
(b `),
b,
a) =
Ros (
(bb `),
bb,
aa)
by RosTrnDef
.=
((Bottom B) "\/" (bb "/\" aa)) "\/" (aa "/\" (bb `))
by LATTICES:20
.=
((bb "/\" aa) "\/" aa) "/\" ((bb "/\" aa) "\/" (bb `))
by LATTICES:11
.=
aa "/\" ((bb "/\" aa) "\/" (bb `))
by LATTICES:def 8
.=
aa "/\" (((bb `) "\/" bb) "/\" ((bb `) "\/" aa))
by LATTICES:11
.=
aa "/\" ((Top B) "/\" ((bb `) "\/" aa))
by LATTICES:21
.=
a
by LATTICES:def 9
;
hence
Tern (
(b `),
b,
a)
= a
;
verum
end;
for a, b being Element of (BA2TBA B) holds Tern (a,b,(b `)) = a
proof
let a,
b be
Element of
(BA2TBA B);
Tern (a,b,(b `)) = a
reconsider aa =
a,
bb =
b as
Element of
B ;
b ` = bb `
by TBACompl;
then Tern (
a,
b,
(b `)) =
Ros (
aa,
bb,
(bb `))
by RosTrnDef
.=
((Bottom B) "\/" (bb "/\" aa)) "\/" (aa "/\" (bb `))
by LATTICES:20
.=
((bb "/\" aa) "\/" aa) "/\" ((bb "/\" aa) "\/" (bb `))
by LATTICES:11
.=
aa "/\" ((bb "/\" aa) "\/" (bb `))
by LATTICES:def 8
.=
aa "/\" (((bb `) "\/" bb) "/\" ((bb `) "\/" aa))
by LATTICES:11
.=
aa "/\" ((Top B) "/\" ((bb `) "\/" aa))
by LATTICES:21
.=
a
by LATTICES:def 9
;
hence
Tern (
a,
b,
(b `))
= a
;
verum
end;
hence
( BA2TBA B is ternary-left-idempotent & BA2TBA B is ternary-right-idempotent & BA2TBA B is ternary-left-absorbing & BA2TBA B is ternary-right-absorbing )
by t1, T4, T5; verum