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
{ b1 where b1 is V8() V9() V10() V14() V15() ext-real non negative finite cardinal V173() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V40() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b1 where b1 is V8() V9() V10() V14() V15() ext-real non negative finite cardinal V173() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{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
{ b1 where b1 is Element of the carrier of T : t in (T,b1) } is set
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
{ b1 where b1 is Element of the of T : t in (T,b1) } is 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
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