:: Automatization of {T}ernary {B}oolean {A}lgebras
:: by Wojciech Ku\'smierowski and Adam Grabowski
::
:: Received September 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct TBAStruct -> ComplStr ;
aggr TBAStruct(# carrier, Compl, TernOp #) -> TBAStruct ;
sel TernOp c₁ -> TriOp of the carrier of c₁;

end;

definition

attr c₁ is strict ;
struct TBALattStr -> TBAStruct , LattStr ;
aggr TBALattStr(# carrier, L_join, L_meet, Compl, TernOp #) -> TBALattStr ;

end;

definition

func op3 -> TriOp of {0} means :: LATTBA_1:def 1
it . (0,0,0) = 0 ;

existence
ex b₁ being TriOp of {0} st b₁ . (0,0,0) = 0

proof end;

uniqueness
for b₁, b₂ being TriOp of {0} st b₁ . (0,0,0) = 0 & b₂ . (0,0,0) = 0 holds
b₁ = b₂ by FUNCT_2:51;

end;

:: deftheorem defines op3 LATTBA_1:def 1 :
for b₁ being TriOp of {0} holds
( b₁ = op3 iff b₁ . (0,0,0) = 0 );

registration

cluster non empty trivial for TBAStruct ;

existence
ex b₁ being TBAStruct st
( b₁ is trivial & not b₁ is empty )

proof end;

end;

definition

let T be non empty TBAStruct ;
let a, b, c be Element of T;

func Tern (a,b,c) -> Element of T equals :: LATTBA_1:def 2
the TernOp of T . (a,b,c);

coherence
the TernOp of T . (a,b,c) is Element of T ;

end;

:: deftheorem defines Tern LATTBA_1:def 2 :
for T being non empty TBAStruct
for a, b, c being Element of T holds Tern (a,b,c) = the TernOp of T . (a,b,c);

definition

let T be non empty TBAStruct ;

attr T is ternary-distributive means :TDis: :: LATTBA_1:def 3
for a, b, c, d, e being Element of T holds Tern ((Tern (a,b,c)),d,(Tern (a,b,e))) = Tern (a,b,(Tern (c,d,e)));

attr T is ternary-left-idempotent means :TLIDef: :: LATTBA_1:def 4
for a, b being Element of T holds Tern (b,b,a) = b;

attr T is ternary-right-idempotent means :TRIDef: :: LATTBA_1:def 5
for a, b being Element of T holds Tern (a,b,b) = b;

attr T is ternary-left-absorbing means :TLADef: :: LATTBA_1:def 6
for a, b being Element of T holds Tern ((b `),b,a) = a;

attr T is ternary-right-absorbing means :TRADef: :: LATTBA_1:def 7
for a, b being Element of T holds Tern (a,b,(b `)) = a;

end;

:: deftheorem TDis defines ternary-distributive LATTBA_1:def 3 :
for T being non empty TBAStruct holds
( T is ternary-distributive iff for a, b, c, d, e being Element of T holds Tern ((Tern (a,b,c)),d,(Tern (a,b,e))) = Tern (a,b,(Tern (c,d,e))) );

:: deftheorem TLIDef defines ternary-left-idempotent LATTBA_1:def 4 :
for T being non empty TBAStruct holds
( T is ternary-left-idempotent iff for a, b being Element of T holds Tern (b,b,a) = b );

:: deftheorem TRIDef defines ternary-right-idempotent LATTBA_1:def 5 :
for T being non empty TBAStruct holds
( T is ternary-right-idempotent iff for a, b being Element of T holds Tern (a,b,b) = b );

:: deftheorem TLADef defines ternary-left-absorbing LATTBA_1:def 6 :
for T being non empty TBAStruct holds
( T is ternary-left-absorbing iff for a, b being Element of T holds Tern ((b `),b,a) = a );

:: deftheorem TRADef defines ternary-right-absorbing LATTBA_1:def 7 :
for T being non empty TBAStruct holds
( T is ternary-right-absorbing iff for a, b being Element of T holds Tern (a,b,(b `)) = a );

:: It seems that only three are enough

registration

cluster non empty trivial -> non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing for TBAStruct ;

coherence
for b₁ being non empty TBAStruct st b₁ is trivial holds
( b₁ is ternary-distributive & b₁ is ternary-left-idempotent & b₁ is ternary-right-idempotent & b₁ is ternary-left-absorbing & b₁ is ternary-right-absorbing ) by STRUCT_0:def 10;

end;

definition

mode Ternary_Boolean_Algebra is non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing TBAStruct ;

end;

:: Section 4 of Grau: Associated Boolean Algebra

definition

let T be Ternary_Boolean_Algebra;
let x be Element of T;

func JoinTBA (T,x) -> BinOp of the carrier of T means :JoinDef: :: LATTBA_1:def 8
for a, b being Element of T holds it . (a,b) = Tern (a,x,b);

existence
ex b₁ being BinOp of the carrier of T st
for a, b being Element of T holds b₁ . (a,b) = Tern (a,x,b)

proof end;

uniqueness
for b₁, b₂ being BinOp of the carrier of T st ( for a, b being Element of T holds b₁ . (a,b) = Tern (a,x,b) ) & ( for a, b being Element of T holds b₂ . (a,b) = Tern (a,x,b) ) holds
b₁ = b₂

proof end;

func MeetTBA (T,x) -> BinOp of the carrier of T means :MeetDef: :: LATTBA_1:def 9
for a, b being Element of T holds it . (a,b) = Tern (a,(x `),b);

existence
ex b₁ being BinOp of the carrier of T st
for a, b being Element of T holds b₁ . (a,b) = Tern (a,(x `),b)

proof end;

uniqueness
for b₁, b₂ being BinOp of the carrier of T st ( for a, b being Element of T holds b₁ . (a,b) = Tern (a,(x `),b) ) & ( for a, b being Element of T holds b<sub>2</sub> . (a,b) = Tern (a,(x `),b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem JoinDef defines JoinTBA LATTBA_1:def 8 :
for T being Ternary_Boolean_Algebra
for x being Element of T
for b₃ being BinOp of the carrier of T holds
( b₃ = JoinTBA (T,x) iff for a, b being Element of T holds b₃ . (a,b) = Tern (a,x,b) );

:: deftheorem MeetDef defines MeetTBA LATTBA_1:def 9 :
for T being Ternary_Boolean_Algebra
for x being Element of T
for b₃ being BinOp of the carrier of T holds
( b₃ = MeetTBA (T,x) iff for a, b being Element of T holds b₃ . (a,b) = Tern (a,(x `),b) );

definition

let T be Ternary_Boolean_Algebra;
let x be Element of T;

func TBA2BA (T,x) -> non empty LattStr equals :: LATTBA_1:def 10
LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #);

correctness
coherence
LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #) is non empty LattStr ;
;

end;

:: deftheorem defines TBA2BA LATTBA_1:def 10 :
for T being Ternary_Boolean_Algebra
for x being Element of T holds TBA2BA (T,x) = LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #);

theorem Th32: :: LATTBA_1:1

for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern (a,b,a) = a

proof end;

theorem Lemma33: :: LATTBA_1:2

for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern ((Tern (a,b,c)),b,a) = Tern (a,b,c)

proof end;

theorem Th33: :: LATTBA_1:3

for T being Ternary_Boolean_Algebra
for a, b, c, d being Element of T holds Tern (a,b,(Tern (c,b,d))) = Tern ((Tern (a,b,c)),b,d)

proof end;

theorem :: LATTBA_1:4

for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern ((b `),b,a) = Tern (a,b,(b `))

proof end;

theorem Lemma34: :: LATTBA_1:5

for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern (a,(b `),b) = a

proof end;

theorem Lemma0: :: LATTBA_1:6

for T being Ternary_Boolean_Algebra
for a being Element of T holds (a `) ` = a

proof end;

theorem Th35: :: LATTBA_1:7

for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern (a,b,(a `)) = b

proof end;

theorem Th36a: :: LATTBA_1:8

for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern (a,b,c) = Tern (a,c,b)

proof end;

theorem Th36b: :: LATTBA_1:9

for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern (a,b,c) = Tern (b,c,a)

proof end;

theorem Th36c: :: LATTBA_1:10

for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern (a,b,c) = Tern (c,b,a)

proof end;

theorem :: LATTBA_1:11

for T being Ternary_Boolean_Algebra
for a, b, c, x being Element of T holds Tern (a,b,c) = Tern ((Tern ((Tern (a,x,b)),(x `),(Tern (b,x,c)))),(x `),(Tern (c,x,a)))

proof end;

definition

let L be B_Lattice;
let a, b, c be Element of L;

func Ros (a,b,c) -> Element of L equals :: LATTBA_1:def 11
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a);

coherence
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) is Element of L ;

end;

:: deftheorem defines Ros LATTBA_1:def 11 :
for L being B_Lattice
for a, b, c being Element of L holds Ros (a,b,c) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a);

definition

let B be B_Lattice;

func RosTrn B -> TriOp of the carrier of B means :RosTrnDef: :: LATTBA_1:def 12
for a, b, c being Element of B holds it . (a,b,c) = Ros (a,b,c);

existence
ex b₁ being TriOp of the carrier of B st
for a, b, c being Element of B holds b₁ . (a,b,c) = Ros (a,b,c)

proof end;

uniqueness
for b₁, b₂ being TriOp of the carrier of B st ( for a, b, c being Element of B holds b₁ . (a,b,c) = Ros (a,b,c) ) & ( for a, b, c being Element of B holds b₂ . (a,b,c) = Ros (a,b,c) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem RosTrnDef defines RosTrn LATTBA_1:def 12 :
for B being B_Lattice
for b₂ being TriOp of the carrier of B holds
( b₂ = RosTrn B iff for a, b, c being Element of B holds b₂ . (a,b,c) = Ros (a,b,c) );

definition

let B be Boolean Lattice;

func BA2TBA B -> TBAStruct equals :: LATTBA_1:def 13
TBAStruct(# the carrier of B,(comp B),(RosTrn B) #);

coherence
TBAStruct(# the carrier of B,(comp B),(RosTrn B) #) is TBAStruct ;

end;

:: deftheorem defines BA2TBA LATTBA_1:def 13 :
for B being Boolean Lattice holds BA2TBA B = TBAStruct(# the carrier of B,(comp B),(RosTrn B) #);

definition

let B be Boolean Lattice;

func BA2TBAA B -> TBALattStr equals :: LATTBA_1:def 14
TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn B) #);

coherence
TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn B) #) is TBALattStr ;

end;

:: deftheorem defines BA2TBAA LATTBA_1:def 14 :
for B being Boolean Lattice holds BA2TBAA B = TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn B) #);

registration

let B be Boolean Lattice;

cluster BA2TBA B -> non empty ;

coherence
not BA2TBA B is empty ;

end;

registration

let B be Boolean Lattice;

cluster BA2TBAA B -> non empty ;

coherence
not BA2TBAA B is empty ;

end;

ThCom: for T being Ternary_Boolean_Algebra
for x, a, b being Element of T holds (JoinTBA (T,x)) . (a,b) = (JoinTBA (T,x)) . (b,a)

proof end;

registration

let T be Ternary_Boolean_Algebra;
let x be Element of T;

cluster JoinTBA (T,x) -> commutative ;

coherence
JoinTBA (T,x) is commutative

proof end;

end;

ThAssoc: for T being Ternary_Boolean_Algebra
for x, a, b, c being Element of T holds (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c)))

proof end;

registration

let T be Ternary_Boolean_Algebra;
let x be Element of T;

cluster JoinTBA (T,x) -> associative ;

coherence
JoinTBA (T,x) is associative

proof end;

end;

ThCom1: for T being Ternary_Boolean_Algebra
for x, a, b being Element of T holds (MeetTBA (T,x)) . (a,b) = (MeetTBA (T,x)) . (b,a)

proof end;

registration

let T be Ternary_Boolean_Algebra;
let x be Element of T;

cluster MeetTBA (T,x) -> commutative ;

coherence
MeetTBA (T,x) is commutative

proof end;

end;

ThV2: for T being Ternary_Boolean_Algebra
for x, a, b, c being Element of T holds (MeetTBA (T,x)) . (((MeetTBA (T,x)) . (a,b)),c) = (MeetTBA (T,x)) . (a,((MeetTBA (T,x)) . (b,c)))

proof end;

registration

let T be Ternary_Boolean_Algebra;
let x be Element of T;

cluster MeetTBA (T,x) -> associative ;

coherence
MeetTBA (T,x) is associative

proof end;

end;

V4: for T being Ternary_Boolean_Algebra
for x being Element of T holds MeetTBA (T,x) absorbs JoinTBA (T,x)

proof end;

V3: for T being Ternary_Boolean_Algebra
for x being Element of T holds JoinTBA (T,x) absorbs MeetTBA (T,x)

proof end;

registration

let T be Ternary_Boolean_Algebra;
let p be Element of T;

cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> Lattice-like ;

coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is Lattice-like

proof end;

end;

registration

let B be Boolean Lattice;

cluster BA2TBAA B -> Lattice-like ;

coherence
BA2TBAA B is Lattice-like

proof end;

end;

theorem TBACompl: :: LATTBA_1:12

for B being Boolean Lattice
for x being Element of B
for xx being Element of (BA2TBA B) st xx = x holds
x ` = xx `

proof end;

theorem TBAComplA: :: LATTBA_1:13

for B being Boolean Lattice
for x being Element of B
for xx being Element of (BA2TBAA B) st xx = x holds
x ` = xx `

proof end;

registration

let B be Boolean Lattice;

cluster BA2TBA B -> ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing ;

coherence
( BA2TBA B is ternary-left-idempotent & BA2TBA B is ternary-right-idempotent & BA2TBA B is ternary-left-absorbing & BA2TBA B is ternary-right-absorbing )

proof end;

end;

registration

let B be Boolean Lattice;

cluster BA2TBAA B -> ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing ;

coherence
( BA2TBAA B is ternary-left-idempotent & BA2TBAA B is ternary-right-idempotent & BA2TBAA B is ternary-left-absorbing & BA2TBAA B is ternary-right-absorbing )

proof end;

end;

theorem TBA1: :: LATTBA_1:14

for B being Boolean Lattice st ( for v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v0,v1) = v0 ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v2,v0,v1) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v0,v2,v1) ) & ( for v3, v2, v1, v0 being Element of (BA2TBAA B) holds Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3))) ) holds
for v1, v2, v3, v4, v5 being Element of (BA2TBAA B) holds Tern ((Tern (v1,v2,v3)),v4,(Tern (v1,v2,v5))) = Tern (v1,v2,(Tern (v3,v4,v5)))

proof end;

theorem TBA2: :: LATTBA_1:15

for B being Boolean Lattice st ( for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) holds
for v1, v2, v3, v4 being Element of (BA2TBAA B) holds Tern ((Tern (v1,v2,v3)),v2,v4) = Tern (v1,v2,(Tern (v3,v2,v4)))

proof end;

LemacikA: for B being Boolean Lattice
for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v2,v0,v1)

proof end;

LemacikB: for B being Boolean Lattice
for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v0,v2,v1)

proof end;

theorem :: LATTBA_1:16

for B being Boolean Lattice
for v0, v1 being Element of (BA2TBAA B)
for a, b being Element of B st a = v0 & b = v1 holds
v0 "\/" v1 = a "\/" b ;

LemacikD: for B being Boolean Lattice
for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)

proof end;

LemacikE: for B being Boolean Lattice
for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2)

proof end;

LemacikC: for B being Boolean Lattice
for v3, v2, v1, v0 being Element of (BA2TBAA B) holds Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3)))

proof end;

registration

let B be Boolean Lattice;

cluster BA2TBAA B -> ternary-distributive ;

coherence
BA2TBAA B is ternary-distributive

proof end;

end;

registration

let T be Ternary_Boolean_Algebra;
let p be Element of T;

cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> distributive ;

coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is distributive

proof end;

end;

registration

let T be Ternary_Boolean_Algebra;
let p be Element of T;

cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> bounded ;

coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is bounded

proof end;

end;

theorem TopTBA: :: LATTBA_1:17

for T being Ternary_Boolean_Algebra
for p being Element of T holds Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p

proof end;

theorem BotTBA: :: LATTBA_1:18

for T being Ternary_Boolean_Algebra
for p being Element of T holds Bottom LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p `

proof end;

registration

let T be Ternary_Boolean_Algebra;
let p be Element of T;

cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> complemented ;

coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is complemented

proof end;

end;

registration

let T be Ternary_Boolean_Algebra;
let p be Element of T;

cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> Boolean ;

coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is Boolean ;

end;

definition

let T be non empty TBAStruct ;

attr T is satisfying_TBA1 means :: LATTBA_1:def 15
for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y;

end;

:: deftheorem defines satisfying_TBA1 LATTBA_1:def 15 :
for T being non empty TBAStruct holds
( T is satisfying_TBA1 iff for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y );

theorem TBALemma: :: LATTBA_1:19

for T being non empty TBAStruct st ( for v4, v3, v2, v1, v0 being Element of T holds Tern ((Tern (v0,v1,v2)),v3,(Tern (v0,v1,v4))) = Tern (v0,v1,(Tern (v2,v3,v4))) ) & ( for v1, v0 being Element of T holds Tern (v0,v1,v1) = v1 ) & ( for v1, v0 being Element of T holds Tern (v0,v1,(v1 `)) = v0 ) & ( for v1, v0 being Element of T holds Tern (v0,v0,v1) = v0 ) holds
for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y

proof end;

definition

let T be non empty TBAStruct ;

attr T is TBA-like means :: LATTBA_1:def 16
( T is ternary-distributive & T is ternary-left-idempotent & T is ternary-right-idempotent & T is ternary-left-absorbing & T is ternary-right-absorbing );

end;

:: deftheorem defines TBA-like LATTBA_1:def 16 :
for T being non empty TBAStruct holds
( T is TBA-like iff ( T is ternary-distributive & T is ternary-left-idempotent & T is ternary-right-idempotent & T is ternary-left-absorbing & T is ternary-right-absorbing ) );

registration

cluster non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing -> non empty TBA-like for TBAStruct ;

coherence
for b₁ being non empty TBAStruct st b₁ is ternary-distributive & b₁ is ternary-left-idempotent & b₁ is ternary-right-idempotent & b₁ is ternary-left-absorbing & b₁ is ternary-right-absorbing holds
b₁ is TBA-like ;

cluster non empty TBA-like -> non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing for TBAStruct ;

coherence
for b₁ being non empty TBAStruct st b₁ is TBA-like holds
( b₁ is ternary-distributive & b₁ is ternary-left-idempotent & b₁ is ternary-right-idempotent & b₁ is ternary-left-absorbing & b₁ is ternary-right-absorbing ) ;

end;

registration

cluster non empty TBA-like -> non empty satisfying_TBA1 for TBAStruct ;

coherence
for b₁ being non empty TBAStruct st b₁ is TBA-like holds
b₁ is satisfying_TBA1

proof end;

end;