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); :: thesis: 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 ; :: thesis: 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); :: thesis: 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 ; :: thesis: 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); :: thesis: 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 ; :: thesis: 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); :: thesis: 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 ; :: thesis: 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; :: thesis: verum