:: ABCMIZ_0 semantic presentation

REAL is set

NAT is non empty non trivial V8() V9() V10() non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty cup-closed diff-closed preBoolean set

NAT is non empty non trivial V8() V9() V10() non finite cardinal limit_cardinal set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

K236() is L6()

the carrier of K236() is set

{} is empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() set

the empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() set is empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() set

1 is non empty V8() V9() V10() V14() V15() ext-real positive non negative finite cardinal V173() Element of NAT

2 is non empty V8() V9() V10() V14() V15() ext-real positive non negative finite cardinal V173() Element of NAT

3 is non empty V8() V9() V10() V14() V15() ext-real positive non negative finite cardinal V173() Element of NAT

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

{ b

{1} is non empty trivial finite V40() 1 -element set

Seg 2 is non empty finite 2 -element Element of bool NAT

{ b

{1,2} is non empty finite V40() set

card {} is empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() set

0 is empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() Element of NAT

T is non empty trivial finite 1 -element RelStr

T is non empty trivial finite 1 -element RelStr

t is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued finite Element of bool [: the carrier of T, the carrier of T:]

the carrier of T is non empty trivial finite 1 -element set

[: the carrier of T, the carrier of T:] is non empty Relation-like finite set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean finite V40() set

field the InternalRel of T is finite set

t2 is non empty set

the Element of t2 is Element of t2

x is set

[ the Element of t2,x] is set

{ the Element of t2,x} is non empty finite set

{ the Element of t2} is non empty trivial finite 1 -element set

{{ the Element of t2,x},{ the Element of t2}} is non empty finite V40() set

the carrier of T \/ the carrier of T is non empty finite set

T is non empty RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

field the InternalRel of T is set

a is non empty Element of bool the carrier of T

the Element of a is Element of a

a /\ (field the InternalRel of T) is Element of bool the carrier of T

X is Element of the carrier of T

y is Element of the carrier of T

[X,y] is Element of [: the carrier of T, the carrier of T:]

{X,y} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,y},{X}} is non empty finite V40() set

y is set

t1 is Element of the carrier of T

t2 is Element of the carrier of T

[t1,t2] is Element of [: the carrier of T, the carrier of T:]

{t1,t2} is non empty finite set

{t1} is non empty trivial finite 1 -element set

{{t1,t2},{t1}} is non empty finite V40() set

a is set

field the InternalRel of T is set

the carrier of T \/ the carrier of T is non empty set

t2 is non empty Element of bool the carrier of T

X is Element of the carrier of T

x is set

[X,x] is set

{X,x} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,x},{X}} is non empty finite V40() set

y is Element of the carrier of T

T is reflexive transitive antisymmetric RelStr

t is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of t is non empty set

the carrier of T is set

a is Element of the carrier of T

t2 is Element of the carrier of T

a "\/" t2 is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr

T is () RelStr

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

the carrier of T is set

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

T is non empty reflexive transitive antisymmetric with_suprema upper-bounded () () RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t is non empty directed lower Element of bool the carrier of T

"\/" (t,T) is Element of the carrier of T

a is Element of the carrier of T

t2 is Element of the carrier of T

a "\/" t2 is Element of the carrier of T

t2 is Element of the carrier of T

T is ()

the of T is set

t is ()

the of t is set

T is ()

the of T is set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

t is Element of the of T

the of T . t is set

dom the of T is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

T is ()

the of T is set

t is ()

the of t is set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

( the of T, the of T) is () ()

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

( the of t, the of t) is () ()

a is Element of the of T

t2 is Element of the of t

(T,a) is Element of the of T

the of T . a is set

(t,t2) is Element of the of t

the of t . t2 is set

T is set

t is set

{T,t} is non empty finite set

a is ()

the of a is set

the of a is Relation-like the of a -defined the of a -valued Function-like V29( the of a) V33( the of a, the of a) Element of bool [: the of a, the of a:]

[: the of a, the of a:] is Relation-like set

bool [: the of a, the of a:] is non empty cup-closed diff-closed preBoolean set

the of a . T is set

the of a . t is set

t2 is Element of the of a

(a,t2) is Element of the of a

the of a . t2 is set

(a,(a,t2)) is Element of the of a

the of a . (a,t2) is set

t2 is Element of the of a

(a,t2) is Element of the of a

the of a . t2 is set

T is ()

the of T is set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

( the of T, the of T) is () ()

t is ()

the of t is set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

( the of t, the of t) is () ()

a is Element of the of t

(t,a) is Element of the of t

the of t . a is set

(t,(t,a)) is Element of the of t

the of t . (t,a) is set

t2 is Element of the of T

(T,t2) is Element of the of T

the of T . t2 is set

(T,(T,t2)) is Element of the of T

the of T . (T,t2) is set

T is ()

the of T is set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

( the of T, the of T) is () ()

t is ()

the of t is set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

( the of t, the of t) is () ()

a is Element of the of t

(t,a) is Element of the of t

the of t . a is set

t2 is Element of the of T

(T,t2) is Element of the of T

the of T . t2 is set

{0,1} is non empty finite V40() Element of bool NAT

[:{0,1},{0,1}:] is non empty Relation-like finite set

bool [:{0,1},{0,1}:] is non empty cup-closed diff-closed preBoolean finite V40() set

t is finite Element of {0,1}

T is finite Element of {0,1}

(0,1) --> (t,T) is non empty Relation-like {0,1} -defined {0,1} -valued Function-like V29({0,1}) V33({0,1},{0,1}) finite Element of bool [:{0,1},{0,1}:]

{0,1} is non empty finite V40() set

[:{0,1},{0,1}:] is non empty Relation-like finite set

bool [:{0,1},{0,1}:] is non empty cup-closed diff-closed preBoolean finite V40() set

a is non empty Relation-like {0,1} -defined {0,1} -valued Function-like V29({0,1}) V33({0,1},{0,1}) finite Element of bool [:{0,1},{0,1}:]

({0,1},a) is () ()

a . t is finite Element of {0,1}

a . T is finite Element of {0,1}

T is () ()

the of T is set

T is non empty set

[:T,T:] is non empty Relation-like set

bool [:T,T:] is non empty cup-closed diff-closed preBoolean set

t is set

[:t,t:] is Relation-like set

bool [:t,t:] is non empty cup-closed diff-closed preBoolean set

Fin t is non empty cup-closed diff-closed preBoolean set

[:T,(Fin t):] is non empty Relation-like set

bool [:T,(Fin t):] is non empty cup-closed diff-closed preBoolean set

a is Relation-like T -defined T -valued Element of bool [:T,T:]

t2 is Relation-like t -defined t -valued Function-like V29(t) V33(t,t) Element of bool [:t,t:]

X is non empty Relation-like T -defined Fin t -valued Function-like V29(T) V33(T, Fin t) Element of bool [:T,(Fin t):]

(T,t,a,t2,X) is () ()

T is set

[:T,T:] is Relation-like set

bool [:T,T:] is non empty cup-closed diff-closed preBoolean set

t is non empty set

[:t,t:] is non empty Relation-like set

bool [:t,t:] is non empty cup-closed diff-closed preBoolean set

Fin t is non empty cup-closed diff-closed preBoolean set

[:T,(Fin t):] is Relation-like set

bool [:T,(Fin t):] is non empty cup-closed diff-closed preBoolean set

a is Relation-like T -defined T -valued Element of bool [:T,T:]

t2 is non empty Relation-like t -defined t -valued Function-like V29(t) V33(t,t) Element of bool [:t,t:]

X is Relation-like T -defined Fin t -valued Function-like V29(T) V33(T, Fin t) Element of bool [:T,(Fin t):]

(T,t,a,t2,X) is () ()

the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr

the () () () () is () () () ()

the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is non empty trivial finite 1 -element set

the of the () () () () is non empty set

Fin the of the () () () () is non empty cup-closed diff-closed preBoolean set

[: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin the of the () () () ()):] is non empty Relation-like set

bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin the of the () () () ()):] is non empty cup-closed diff-closed preBoolean set

the non empty Relation-like the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -defined Fin the of the () () () () -valued Function-like V29( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ) V33( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , Fin the of the () () () ()) finite Element of bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin the of the () () () ()):] is non empty Relation-like the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -defined Fin the of the () () () () -valued Function-like V29( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ) V33( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , Fin the of the () () () ()) finite Element of bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin the of the () () () ()):]

the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is Relation-like the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -defined the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -valued finite co-well_founded Element of bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr :]

[: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr :] is non empty Relation-like finite set

bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr :] is non empty cup-closed diff-closed preBoolean finite V40() set

the of the () () () () is non empty Relation-like the of the () () () () -defined the of the () () () () -valued Function-like V29( the of the () () () ()) V33( the of the () () () (), the of the () () () ()) Element of bool [: the of the () () () (), the of the () () () ():]

[: the of the () () () (), the of the () () () ():] is non empty Relation-like set

bool [: the of the () () () (), the of the () () () ():] is non empty cup-closed diff-closed preBoolean set

( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the of the () () () (), the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the of the () () () (), the non empty Relation-like the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -defined Fin the of the () () () () -valued Function-like V29( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ) V33( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , Fin the of the () () () ()) finite Element of bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin the of the () () () ()):]) is non empty () () ()

t2 is non empty () () ()

the carrier of t2 is non empty set

RelStr(# the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr #) is strict RelStr

the InternalRel of t2 is Relation-like the carrier of t2 -defined the carrier of t2 -valued Element of bool [: the carrier of t2, the carrier of t2:]

[: the carrier of t2, the carrier of t2:] is non empty Relation-like set

bool [: the carrier of t2, the carrier of t2:] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of t2, the InternalRel of t2 #) is strict RelStr

( the of the () () () (), the of the () () () ()) is () ()

the of t2 is non empty set

the of t2 is non empty Relation-like the of t2 -defined the of t2 -valued Function-like V29( the of t2) V33( the of t2, the of t2) Element of bool [: the of t2, the of t2:]

[: the of t2, the of t2:] is non empty Relation-like set

bool [: the of t2, the of t2:] is non empty cup-closed diff-closed preBoolean set

( the of t2, the of t2) is () ()

T is ()

the carrier of T is set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

the of T is set

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

t is Element of the carrier of T

the of T . t is set

bool the of T is non empty cup-closed diff-closed preBoolean set

dom the of T is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

{} the of T is empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() Element of bool the of T

T is ()

the carrier of T is set

t is ()

the carrier of t is set

the of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

( the carrier of T, the of T, the InternalRel of T, the of T, the of T) is () ()

the of t is set

the InternalRel of t is Relation-like the carrier of t -defined the carrier of t -valued Element of bool [: the carrier of t, the carrier of t:]

[: the carrier of t, the carrier of t:] is Relation-like set

bool [: the carrier of t, the carrier of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the carrier of t -defined Fin the of t -valued Function-like V29( the carrier of t) V33( the carrier of t, Fin the of t) Element of bool [: the carrier of t,(Fin the of t):]

Fin the of t is non empty cup-closed diff-closed preBoolean set

[: the carrier of t,(Fin the of t):] is Relation-like set

bool [: the carrier of t,(Fin the of t):] is non empty cup-closed diff-closed preBoolean set

( the carrier of t, the of t, the InternalRel of t, the of t, the of t) is () ()

a is Element of the carrier of T

t2 is Element of the carrier of t

(T,a) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T . a is set

(t,t2) is Element of bool the of t

bool the of t is non empty cup-closed diff-closed preBoolean set

the of t . t2 is set

T is ()

the carrier of T is set

the of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

( the carrier of T, the of T, the InternalRel of T, the of T, the of T) is () ()

t is ()

the carrier of t is set

the of t is set

the InternalRel of t is Relation-like the carrier of t -defined the carrier of t -valued Element of bool [: the carrier of t, the carrier of t:]

[: the carrier of t, the carrier of t:] is Relation-like set

bool [: the carrier of t, the carrier of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the carrier of t -defined Fin the of t -valued Function-like V29( the carrier of t) V33( the carrier of t, Fin the of t) Element of bool [: the carrier of t,(Fin the of t):]

Fin the of t is non empty cup-closed diff-closed preBoolean set

[: the carrier of t,(Fin the of t):] is Relation-like set

bool [: the carrier of t,(Fin the of t):] is non empty cup-closed diff-closed preBoolean set

( the carrier of t, the of t, the InternalRel of t, the of t, the of t) is () ()

a is Element of the carrier of t

(t,a) is Element of bool the of t

bool the of t is non empty cup-closed diff-closed preBoolean set

the of t . a is set

t2 is Element of the of t

(t,t2) is Element of the of t

the of t . t2 is set

X is Element of the of T

(T,X) is Element of the of T

the of T . X is set

x is Element of the carrier of T

(T,x) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T . x is set

T is non empty ()

the carrier of T is non empty set

the of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

( the carrier of T, the of T, the InternalRel of T, the of T, the of T) is non empty () ()

t is non empty ()

the carrier of t is non empty set

the of t is set

the InternalRel of t is Relation-like the carrier of t -defined the carrier of t -valued Element of bool [: the carrier of t, the carrier of t:]

[: the carrier of t, the carrier of t:] is non empty Relation-like set

bool [: the carrier of t, the carrier of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

the of t is non empty Relation-like the carrier of t -defined Fin the of t -valued Function-like V29( the carrier of t) V33( the carrier of t, Fin the of t) Element of bool [: the carrier of t,(Fin the of t):]

Fin the of t is non empty cup-closed diff-closed preBoolean set

[: the carrier of t,(Fin the of t):] is non empty Relation-like set

bool [: the carrier of t,(Fin the of t):] is non empty cup-closed diff-closed preBoolean set

( the carrier of t, the of t, the InternalRel of t, the of t, the of t) is non empty () ()

BoolePoset the of T is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete RelStr

(BoolePoset the of T) ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete RelStr

the carrier of (BoolePoset the of T) is non empty set

the InternalRel of (BoolePoset the of T) is Relation-like the carrier of (BoolePoset the of T) -defined the carrier of (BoolePoset the of T) -valued Element of bool [: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):]

[: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):] is non empty Relation-like set

bool [: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):] is non empty cup-closed diff-closed preBoolean set

the InternalRel of (BoolePoset the of T) ~ is Relation-like the carrier of (BoolePoset the of T) -defined the carrier of (BoolePoset the of T) -valued Element of bool [: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):]

RelStr(# the carrier of (BoolePoset the of T),( the InternalRel of (BoolePoset the of T) ~) #) is strict RelStr

the carrier of ((BoolePoset the of T) ~) is non empty set

[: the carrier of T, the carrier of ((BoolePoset the of T) ~):] is non empty Relation-like set

bool [: the carrier of T, the carrier of ((BoolePoset the of T) ~):] is non empty cup-closed diff-closed preBoolean set

BoolePoset the of t is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete RelStr

(BoolePoset the of t) ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete RelStr

the carrier of (BoolePoset the of t) is non empty set

the InternalRel of (BoolePoset the of t) is Relation-like the carrier of (BoolePoset the of t) -defined the carrier of (BoolePoset the of t) -valued Element of bool [: the carrier of (BoolePoset the of t), the carrier of (BoolePoset the of t):]

[: the carrier of (BoolePoset the of t), the carrier of (BoolePoset the of t):] is non empty Relation-like set

bool [: the carrier of (BoolePoset the of t), the carrier of (BoolePoset the of t):] is non empty cup-closed diff-closed preBoolean set

the InternalRel of (BoolePoset the of t) ~ is Relation-like the carrier of (BoolePoset the of t) -defined the carrier of (BoolePoset the of t) -valued Element of bool [: the carrier of (BoolePoset the of t), the carrier of (BoolePoset the of t):]

RelStr(# the carrier of (BoolePoset the of t),( the InternalRel of (BoolePoset the of t) ~) #) is strict RelStr

the carrier of ((BoolePoset the of t) ~) is non empty set

[: the carrier of t, the carrier of ((BoolePoset the of t) ~):] is non empty Relation-like set

bool [: the carrier of t, the carrier of ((BoolePoset the of t) ~):] is non empty cup-closed diff-closed preBoolean set

a is non empty Relation-like the carrier of T -defined the carrier of ((BoolePoset the of T) ~) -valued Function-like V29( the carrier of T) V33( the carrier of T, the carrier of ((BoolePoset the of T) ~)) join-preserving Element of bool [: the carrier of T, the carrier of ((BoolePoset the of T) ~):]

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

RelStr(# the carrier of t, the InternalRel of t #) is strict RelStr

t2 is non empty Relation-like the carrier of t -defined the carrier of ((BoolePoset the of t) ~) -valued Function-like V29( the carrier of t) V33( the carrier of t, the carrier of ((BoolePoset the of t) ~)) Element of bool [: the carrier of t, the carrier of ((BoolePoset the of t) ~):]

X is Element of the carrier of t

x is Element of the carrier of t

{X,x} is non empty finite Element of bool the carrier of t

bool the carrier of t is non empty cup-closed diff-closed preBoolean set

t2 .: {X,x} is finite Element of bool the carrier of ((BoolePoset the of t) ~)

bool the carrier of ((BoolePoset the of t) ~) is non empty cup-closed diff-closed preBoolean set

"\/" ((t2 .: {X,x}),((BoolePoset the of t) ~)) is Element of the carrier of ((BoolePoset the of t) ~)

"\/" ({X,x},t) is Element of the carrier of t

t2 . ("\/" ({X,x},t)) is Element of the carrier of ((BoolePoset the of t) ~)

y is Element of the carrier of T

t1 is Element of the carrier of T

{y,t1} is non empty finite Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

a .: {y,t1} is finite Element of bool the carrier of ((BoolePoset the of T) ~)

bool the carrier of ((BoolePoset the of T) ~) is non empty cup-closed diff-closed preBoolean set

"\/" ((a .: {y,t1}),((BoolePoset the of T) ~)) is Element of the carrier of ((BoolePoset the of T) ~)

"\/" ({y,t1},T) is Element of the carrier of T

a . ("\/" ({y,t1},T)) is Element of the carrier of ((BoolePoset the of T) ~)

T is non empty reflexive transitive antisymmetric with_suprema ()

the carrier of T is non empty set

the of T is set

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

dom the of T is non empty Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

BoolePoset the of T is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete RelStr

InclPoset (bool the of T) is non empty strict reflexive transitive antisymmetric RelStr

RelIncl (bool the of T) is Relation-like bool the of T -defined bool the of T -valued V29( bool the of T) V33( bool the of T, bool the of T) reflexive antisymmetric transitive Element of bool [:(bool the of T),(bool the of T):]

[:(bool the of T),(bool the of T):] is non empty Relation-like set

bool [:(bool the of T),(bool the of T):] is non empty cup-closed diff-closed preBoolean set

RelStr(# (bool the of T),(RelIncl (bool the of T)) #) is strict RelStr

rng the of T is non empty Element of bool (Fin the of T)

bool (Fin the of T) is non empty cup-closed diff-closed preBoolean set

(BoolePoset the of T) ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete RelStr

the carrier of (BoolePoset the of T) is non empty set

the InternalRel of (BoolePoset the of T) is Relation-like the carrier of (BoolePoset the of T) -defined the carrier of (BoolePoset the of T) -valued Element of bool [: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):]

[: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):] is non empty Relation-like set

bool [: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):] is non empty cup-closed diff-closed preBoolean set

the InternalRel of (BoolePoset the of T) ~ is Relation-like the carrier of (BoolePoset the of T) -defined the carrier of (BoolePoset the of T) -valued Element of bool [: the carrier of (BoolePoset the of T), the carrier of (BoolePoset the of T):]

RelStr(# the carrier of (BoolePoset the of T),( the InternalRel of (BoolePoset the of T) ~) #) is strict RelStr

the carrier of ((BoolePoset the of T) ~) is non empty set

[: the carrier of T, the carrier of ((BoolePoset the of T) ~):] is non empty Relation-like set

bool [: the carrier of T, the carrier of ((BoolePoset the of T) ~):] is non empty cup-closed diff-closed preBoolean set

t2 is Element of the carrier of T

X is Element of the carrier of T

t2 "\/" X is Element of the carrier of T

(T,(t2 "\/" X)) is Element of bool the of T

the of T . (t2 "\/" X) is set

(T,t2) is Element of bool the of T

the of T . t2 is set

(T,X) is Element of bool the of T

the of T . X is set

(T,t2) /\ (T,X) is Element of bool the of T

a is non empty Relation-like the carrier of T -defined the carrier of ((BoolePoset the of T) ~) -valued Function-like V29( the carrier of T) V33( the carrier of T, the carrier of ((BoolePoset the of T) ~)) join-preserving Element of bool [: the carrier of T, the carrier of ((BoolePoset the of T) ~):]

a . t2 is Element of the carrier of ((BoolePoset the of T) ~)

a . X is Element of the carrier of ((BoolePoset the of T) ~)

(a . t2) "\/" (a . X) is Element of the carrier of ((BoolePoset the of T) ~)

~ (a . t2) is Element of the carrier of (BoolePoset the of T)

~ (a . X) is Element of the carrier of (BoolePoset the of T)

(~ (a . t2)) "/\" (~ (a . X)) is Element of the carrier of (BoolePoset the of T)

t is non empty Relation-like the carrier of T -defined the carrier of ((BoolePoset the of T) ~) -valued Function-like V29( the carrier of T) V33( the carrier of T, the carrier of ((BoolePoset the of T) ~)) Element of bool [: the carrier of T, the carrier of ((BoolePoset the of T) ~):]

a is Element of the carrier of T

t2 is Element of the carrier of T

a "\/" t2 is Element of the carrier of T

t . (a "\/" t2) is Element of the carrier of ((BoolePoset the of T) ~)

(T,(a "\/" t2)) is Element of bool the of T

the of T . (a "\/" t2) is set

(T,a) is Element of bool the of T

the of T . a is set

(T,t2) is Element of bool the of T

the of T . t2 is set

(T,a) /\ (T,t2) is Element of bool the of T

t . a is Element of the carrier of ((BoolePoset the of T) ~)

~ (t . a) is Element of the carrier of (BoolePoset the of T)

t . t2 is Element of the carrier of ((BoolePoset the of T) ~)

~ (t . t2) is Element of the carrier of (BoolePoset the of T)

(~ (t . a)) "/\" (~ (t . t2)) is Element of the carrier of (BoolePoset the of T)

(t . a) "\/" (t . t2) is Element of the carrier of ((BoolePoset the of T) ~)

T is non empty reflexive transitive antisymmetric with_suprema ()

the carrier of T is non empty set

the of T is set

bool the of T is non empty cup-closed diff-closed preBoolean set

t is Element of the carrier of T

a is Element of the carrier of T

(T,a) is Element of bool the of T

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . a is set

(T,t) is Element of bool the of T

the of T . t is set

t "\/" a is Element of the carrier of T

(T,t) /\ (T,a) is Element of bool the of T

T is ()

the of T is set

the carrier of T is set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t is Element of the of T

a is set

t2 is set

t2 is Element of bool the carrier of T

X is set

x is Element of the carrier of T

(T,x) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . x is set

dom the of T is Element of bool the carrier of T

a is Element of bool the carrier of T

t2 is Element of bool the carrier of T

T is non empty ()

the of T is set

bool the of T is non empty cup-closed diff-closed preBoolean set

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t is Element of bool the of T

a is set

t2 is set

t2 is Element of bool the carrier of T

X is Element of the carrier of T

x is Element of the of T

(T,x) is Element of bool the carrier of T

y is Element of the carrier of T

a is Element of bool the carrier of T

t2 is Element of bool the carrier of T

X is set

x is Element of the of T

(T,x) is Element of bool the carrier of T

x is Element of the of T

(T,x) is Element of bool the carrier of T

T is ()

the carrier of T is set

the of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

( the carrier of T, the of T, the InternalRel of T, the of T, the of T) is () ()

t is ()

the carrier of t is set

the of t is set

the InternalRel of t is Relation-like the carrier of t -defined the carrier of t -valued Element of bool [: the carrier of t, the carrier of t:]

[: the carrier of t, the carrier of t:] is Relation-like set

bool [: the carrier of t, the carrier of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the carrier of t -defined Fin the of t -valued Function-like V29( the carrier of t) V33( the carrier of t, Fin the of t) Element of bool [: the carrier of t,(Fin the of t):]

Fin the of t is non empty cup-closed diff-closed preBoolean set

[: the carrier of t,(Fin the of t):] is Relation-like set

bool [: the carrier of t,(Fin the of t):] is non empty cup-closed diff-closed preBoolean set

( the carrier of t, the of t, the InternalRel of t, the of t, the of t) is () ()

a is Element of the of T

(T,a) is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t2 is Element of the of t

(t,t2) is Element of bool the carrier of t

bool the carrier of t is non empty cup-closed diff-closed preBoolean set

X is set

x is Element of the carrier of T

(T,x) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T . x is set

y is Element of the carrier of t

(t,y) is Element of bool the of t

bool the of t is non empty cup-closed diff-closed preBoolean set

the of t . y is set

x is Element of the carrier of t

(t,x) is Element of bool the of t

the of t . x is set

y is Element of the carrier of T

(T,y) is Element of bool the of T

the of T . y is set

T is non empty ()

the of T is set

the carrier of T is non empty set

t is Element of the of T

(T,t) is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

{ b

t2 is set

X is Element of the carrier of T

(T,X) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . X is set

t2 is Element of bool the carrier of T

X is set

x is set

y is Element of the carrier of T

(T,y) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . y is set

T is ()

the carrier of T is set

the of T is set

t is Element of the carrier of T

(T,t) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . t is set

a is Element of the of T

(T,a) is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t2 is Element of the carrier of T

(T,t2) is Element of bool the of T

the of T . t2 is set

T is non empty ()

the carrier of T is non empty set

the of T is set

bool the of T is non empty cup-closed diff-closed preBoolean set

t is Element of the carrier of T

(T,t) is Element of bool the of T

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . t is set

a is Element of bool the of T

(T,a) is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t2 is Element of the of T

(T,t2) is Element of bool the carrier of T

t2 is set

X is Element of the of T

(T,X) is Element of bool the carrier of T

T is () ()

the carrier of T is set

the of T is non empty set

t is Element of the carrier of T

(T,t) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . t is set

{ b

t2 is set

X is Element of the of T

(T,X) is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t2 is set

X is Element of the of T

(T,X) is Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

T is non empty ()

the of T is set

{} the of T is empty V8() V9() V10() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding functional finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete irreflexive V173() Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

(T,({} the of T)) is Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t is set

a is Element of the carrier of T

t2 is Element of the of T

(T,t2) is Element of bool the carrier of T

T is ()

the carrier of T is set

the of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

( the carrier of T, the of T, the InternalRel of T, the of T, the of T) is () ()

t is ()

the carrier of t is set

the of t is set

the InternalRel of t is Relation-like the carrier of t -defined the carrier of t -valued Element of bool [: the carrier of t, the carrier of t:]

[: the carrier of t, the carrier of t:] is Relation-like set

bool [: the carrier of t, the carrier of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the of t -defined the of t -valued Function-like V29( the of t) V33( the of t, the of t) Element of bool [: the of t, the of t:]

[: the of t, the of t:] is Relation-like set

bool [: the of t, the of t:] is non empty cup-closed diff-closed preBoolean set

the of t is Relation-like the carrier of t -defined Fin the of t -valued Function-like V29( the carrier of t) V33( the carrier of t, Fin the of t) Element of bool [: the carrier of t,(Fin the of t):]

Fin the of t is non empty cup-closed diff-closed preBoolean set

[: the carrier of t,(Fin the of t):] is Relation-like set

bool [: the carrier of t,(Fin the of t):] is non empty cup-closed diff-closed preBoolean set

( the carrier of t, the of t, the InternalRel of t, the of t, the of t) is () ()

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

bool the carrier of t is non empty cup-closed diff-closed preBoolean set

a is Element of the of t

(t,a) is Element of bool the carrier of t

(t,a) is Element of the of t

the of t . a is set

(t,(t,a)) is Element of bool the carrier of t

(t,a) \/ (t,(t,a)) is Element of bool the carrier of t

t2 is Element of the of T

(T,t2) is Element of bool the carrier of T

(T,t2) is Element of the of T

the of T . t2 is set

(T,(T,t2)) is Element of bool the carrier of T

(T,t2) \/ (T,(T,t2)) is Element of bool the carrier of T

{0} is non empty trivial finite V40() 1 -element Element of bool NAT

{0,1} is non empty finite V40() Element of bool NAT

Fin {0,1} is non empty cup-closed diff-closed preBoolean set

the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr

[:{0,1},{0,1}:] is non empty Relation-like finite set

bool [:{0,1},{0,1}:] is non empty cup-closed diff-closed preBoolean finite V40() set

a is finite Element of {0,1}

t is finite Element of {0,1}

(0,1) --> (a,t) is non empty Relation-like {0,1} -defined {0,1} -valued Function-like V29({0,1}) V33({0,1},{0,1}) finite Element of bool [:{0,1},{0,1}:]

{0,1} is non empty finite V40() set

[:{0,1},{0,1}:] is non empty Relation-like finite set

bool [:{0,1},{0,1}:] is non empty cup-closed diff-closed preBoolean finite V40() set

the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is non empty trivial finite 1 -element set

T is finite Element of Fin {0,1}

the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T is non empty Relation-like the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -defined Fin {0,1} -valued Function-like V29( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ) V33( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , Fin {0,1}) finite Element of bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin {0,1}):]

[: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin {0,1}):] is non empty Relation-like set

bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,(Fin {0,1}):] is non empty cup-closed diff-closed preBoolean set

the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr is Relation-like the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -defined the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr -valued finite co-well_founded Element of bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr :]

[: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr :] is non empty Relation-like finite set

bool [: the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr :] is non empty cup-closed diff-closed preBoolean finite V40() set

X is non empty Relation-like {0,1} -defined {0,1} -valued Function-like V29({0,1}) V33({0,1},{0,1}) finite Element of bool [:{0,1},{0,1}:]

( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)) is non empty () () ()

the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)) is non empty set

the InternalRel of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)) is Relation-like the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)) -defined the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)) -valued Element of bool [: the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)), the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)):]

[: the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)), the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)):] is non empty Relation-like set

bool [: the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)), the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)):] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)), the InternalRel of ( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,{0,1}, the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr ,X,( the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr --> T)) #) is strict RelStr

RelStr(# the carrier of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr , the InternalRel of the non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () RelStr #) is strict RelStr

t1 is non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete () () () ()

X . a is finite Element of {0,1}

X . t is finite Element of {0,1}

the carrier of t1 is non empty trivial finite 1 -element set

the of t1 is set

t2 is Element of the carrier of t1

(t1,t2) is Element of bool the of t1

bool the of t1 is non empty cup-closed diff-closed preBoolean set

the of t1 is non empty Relation-like the carrier of t1 -defined Fin the of t1 -valued Function-like V29( the carrier of t1) V33( the carrier of t1, Fin the of t1) finite Element of bool [: the carrier of t1,(Fin the of t1):]

Fin the of t1 is non empty cup-closed diff-closed preBoolean set

[: the carrier of t1,(Fin the of t1):] is non empty Relation-like set

bool [: the carrier of t1,(Fin the of t1):] is non empty cup-closed diff-closed preBoolean set

the of t1 . t2 is set

v2 is Element of the of t1

(t1,v2) is Element of the of t1

the of t1 is Relation-like the of t1 -defined the of t1 -valued Function-like V29( the of t1) V33( the of t1, the of t1) Element of bool [: the of t1, the of t1:]

[: the of t1, the of t1:] is Relation-like set

bool [: the of t1, the of t1:] is non empty cup-closed diff-closed preBoolean set

the of t1 . v2 is set

the Element of the carrier of t1 is Element of the carrier of t1

a3 is Element of the carrier of t1

(t1,a3) is Element of bool the of t1

the of t1 . a3 is set

v2 is Element of the carrier of t1

(t1,v2) is Element of bool the of t1

the of t1 . v2 is set

v2 "\/" a3 is Element of the carrier of t1

(t1,(v2 "\/" a3)) is Element of bool the of t1

the of t1 . (v2 "\/" a3) is set

(t1,v2) /\ (t1,a3) is Element of bool the of t1

bool the carrier of t1 is non empty cup-closed diff-closed preBoolean finite V40() set

v2 is Element of the of t1

(t1,v2) is trivial finite Element of bool the carrier of t1

(t1,v2) is Element of the of t1

the of t1 . v2 is set

(t1,(t1,v2)) is trivial finite Element of bool the carrier of t1

(t1,v2) \/ (t1,(t1,v2)) is trivial finite Element of bool the carrier of t1

(t1, the Element of the carrier of t1) is Element of bool the of t1

the of t1 . the Element of the carrier of t1 is set

T is () ()

the of T is set

t is Element of the of T

(T,t) is Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

(T,t) is Element of the of T

the of T is Relation-like the of T -defined the of T -valued Function-like V29( the of T) V33( the of T, the of T) Element of bool [: the of T, the of T:]

[: the of T, the of T:] is Relation-like set

bool [: the of T, the of T:] is non empty cup-closed diff-closed preBoolean set

the of T . t is set

(T,(T,t)) is Element of bool the carrier of T

a is set

t2 is Element of the carrier of T

(T,t2) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . t2 is set

X is Element of the carrier of T

(T,X) is Element of bool the of T

the of T . X is set

T is non empty reflexive transitive antisymmetric with_suprema () ()

the of T is set

t is Element of the of T

(T,t) is Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

a is Element of the carrier of T

t2 is Element of the carrier of T

(T,a) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . a is set

(T,t2) is Element of bool the of T

the of T . t2 is set

a is Element of the carrier of T

t2 is Element of the carrier of T

a "\/" t2 is Element of the carrier of T

(T,t2) is Element of bool the of T

bool the of T is non empty cup-closed diff-closed preBoolean set

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . t2 is set

(T,a) is Element of bool the of T

the of T . a is set

(T,a) /\ (T,t2) is Element of bool the of T

(T,(a "\/" t2)) is Element of bool the of T

the of T . (a "\/" t2) is set

T is non empty reflexive transitive antisymmetric with_suprema () ()

the of T is set

bool the of T is non empty cup-closed diff-closed preBoolean set

t is Element of bool the of T

(T,t) is Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

a is Element of the carrier of T

t2 is Element of the carrier of T

X is Element of the of T

(T,X) is directed lower Element of bool the carrier of T

(T,a) is Element of bool the of T

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . a is set

(T,t2) is Element of bool the of T

the of T . t2 is set

a is Element of the carrier of T

t2 is Element of the carrier of T

a "\/" t2 is Element of the carrier of T

X is Element of the of T

(T,X) is directed lower Element of bool the carrier of T

(T,t2) is Element of bool the of T

the of T is non empty Relation-like the carrier of T -defined Fin the of T -valued Function-like V29( the carrier of T) V33( the carrier of T, Fin the of T) Element of bool [: the carrier of T,(Fin the of T):]

Fin the of T is non empty cup-closed diff-closed preBoolean set

[: the carrier of T,(Fin the of T):] is non empty Relation-like set

bool [: the carrier of T,(Fin the of T):] is non empty cup-closed diff-closed preBoolean set

the of T . t2 is set

(T,a) is Element of bool the of T

the of T . a is set

(T,a) /\ (T,t2) is Element of bool the of T

(T,(a "\/" t2)) is Element of bool the of T

the of T . (a "\/" t2) is set

T is ()

the carrier of T is set

the of T is set

T is ()

the carrier of T is set

the of T is set

bool the of T is non empty cup-closed diff-closed preBoolean set

T is non empty reflexive transitive antisymmetric with_suprema () ()

the of T is set

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

t is Element of the of T

(T,t) is directed lower Element of bool the carrier of T

a is Element of the carrier of T

downarrow a is non empty directed lower Element of bool the carrier of T

{a} is non empty trivial finite 1 -element Element of bool the carrier of T

downarrow {a} is non empty lower Element of bool the carrier of T

(T,t) /\ (downarrow a) is Element of bool the carrier of T

t2 is Element of the carrier of T

T is non empty reflexive transitive ()

the carrier of T is non empty set

the of T is set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

a is Element of the of T

(T,a) is Element of bool the carrier of T

t is Element of the carrier of T

downarrow t is non empty directed lower Element of bool the carrier of T

{t} is non empty trivial finite 1 -element Element of bool the carrier of T

downarrow {t} is non empty lower Element of bool the carrier of T

(T,a) /\ (downarrow t) is Element of bool the carrier of T

"\/" (((T,a) /\ (downarrow t)),T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema upper-bounded () () () ()

the carrier of T is non empty set

the of T is set

t is Element of the carrier of T

a is Element of the of T

(T,t,a) is Element of the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

(T,a) is directed lower Element of bool the carrier of T

downarrow t is non empty directed lower Element of bool the carrier of T

{t} is non empty trivial finite 1 -element Element of bool the carrier of T

downarrow {t} is non empty lower Element of bool the carrier of T

(T,a) /\ (downarrow t) is Element of bool the carrier of T

"\/" (((T,a) /\ (downarrow t)),T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema upper-bounded () () () ()

the carrier of T is non empty set

the of T is set

t is Element of the carrier of T

a is Element of the of T

(T,t,a) is Element of the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

(T,a) is directed lower Element of bool the carrier of T

downarrow t is non empty directed lower Element of bool the carrier of T

{t} is non empty trivial finite 1 -element Element of bool the carrier of T

downarrow