:: YELLOW_1 semantic presentation

K218() is set
K222() is non empty V12() V13() V14() V42() V47() V48() Element of bool K218()
bool K218() is non empty set
K46() is non empty V12() V13() V14() V42() V47() V48() set
bool K46() is non empty V42() set
bool K222() is non empty V42() set
K267() is set
{} is empty V12() V13() V14() V16() V17() V18() V42() V47() V49( {} ) set
the empty V12() V13() V14() V16() V17() V18() V42() V47() V49( {} ) set is empty V12() V13() V14() V16() V17() V18() V42() V47() V49( {} ) set
{{}} is non empty trivial V49(1) set
1 is non empty V12() V13() V14() V18() V42() V47() Element of K222()
K245({{}}) is M18({{}})
[:K245({{}}),{{}}:] is set
bool [:K245({{}}),{{}}:] is non empty set
K58(K245({{}}),{{}}) is non empty functional set
{{},1} is non empty set
product {} is set
S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet S is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
LattPOSet S is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (LattPOSet S) is non empty set
Top (LattPOSet S) is Element of the carrier of (LattPOSet S)
T is Element of the carrier of (LattPOSet S)
A1 is Element of the carrier of S
Top S is Element of the carrier of S
a is Element of the carrier of (LattPOSet S)
f is Element of the carrier of S
f % is Element of the carrier of (LattPOSet S)
A1 % is Element of the carrier of (LattPOSet S)
A2 is Element of the carrier of (LattPOSet S)
"/\" ({},(LattPOSet S)) is Element of the carrier of (LattPOSet S)
f is Element of the carrier of (LattPOSet S)
x9 is Element of the carrier of S
a is Element of the carrier of S
x9 % is Element of the carrier of (LattPOSet S)
a % is Element of the carrier of (LattPOSet S)
T is Element of the carrier of (LattPOSet S)
S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
LattPOSet S is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (LattPOSet S) is non empty set
Bottom (LattPOSet S) is Element of the carrier of (LattPOSet S)
T is Element of the carrier of (LattPOSet S)
A1 is Element of the carrier of S
Bottom S is Element of the carrier of S
a is Element of the carrier of (LattPOSet S)
f is Element of the carrier of S
f % is Element of the carrier of (LattPOSet S)
A1 % is Element of the carrier of (LattPOSet S)
A2 is Element of the carrier of (LattPOSet S)
"\/" ({},(LattPOSet S)) is Element of the carrier of (LattPOSet S)
f is Element of the carrier of (LattPOSet S)
a is Element of the carrier of S
x9 is Element of the carrier of S
x9 % is Element of the carrier of (LattPOSet S)
a % is Element of the carrier of (LattPOSet S)
T is Element of the carrier of (LattPOSet S)
S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
LattPOSet S is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (LattPOSet S) is non empty set
T is set
"\/" (T,(LattPOSet S)) is Element of the carrier of (LattPOSet S)
A1 is Element of the carrier of (LattPOSet S)
"\/" (T,S) is Element of the carrier of S
("\/" (T,S)) % is Element of the carrier of (LattPOSet S)
A2 is Element of the carrier of (LattPOSet S)
a is Element of the carrier of S
a % is Element of the carrier of (LattPOSet S)
S is set
RelIncl S is Relation-like reflexive antisymmetric transitive set
[:S,S:] is set
bool [:S,S:] is non empty set
T is set
A1 is set
A2 is set
[A1,A2] is set
{A1,A2} is non empty set
{A1} is non empty trivial V49(1) set
{{A1,A2},{A1}} is non empty set
field (RelIncl S) is set
dom (RelIncl S) is set
rng (RelIncl S) is set
(dom (RelIncl S)) \/ (rng (RelIncl S)) is set
T is Relation-like S -defined S -valued Element of bool [:S,S:]
field T is set
dom T is set
rng T is set
(dom T) \/ (rng T) is set
dom T is Element of bool S
bool S is non empty set
S is set
(S) is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is strict RelStr
(S) is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is strict V84() reflexive transitive antisymmetric RelStr
S is non empty set
(S) is strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is strict V84() reflexive transitive antisymmetric RelStr
(S) is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is set
T is set
(T) is strict V84() reflexive transitive antisymmetric RelStr
(T) is Relation-like T -defined T -valued reflexive antisymmetric transitive V34(T) Element of bool [:T,T:]
[:T,T:] is set
bool [:T,T:] is non empty set
RelStr(# T,(T) #) is strict V84() reflexive transitive antisymmetric RelStr
the InternalRel of (T) is Relation-like the carrier of (T) -defined the carrier of (T) -valued reflexive antisymmetric transitive V34( the carrier of (T)) 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 set
bool [: the carrier of (T), the carrier of (T):] is non empty set
S is set
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is strict RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
A2 is Element of the carrier of (BooleLatt S)
A2 % is Element of the carrier of (LattPOSet (BooleLatt S))
the carrier of (LattPOSet (BooleLatt S)) is non empty set
a is Element of the carrier of (BooleLatt S)
a % is Element of the carrier of (LattPOSet (BooleLatt S))
A2 is Element of the carrier of (BooleLatt S)
a is Element of the carrier of (BooleLatt S)
A2 % is Element of the carrier of (LattPOSet (BooleLatt S))
the carrier of (LattPOSet (BooleLatt S)) is non empty set
a % is Element of the carrier of (LattPOSet (BooleLatt S))
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
[T,A1] is set
{T,A1} is non empty set
{T} is non empty trivial V49(1) set
{{T,A1},{T}} is non empty set
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued reflexive antisymmetric transitive V34( the carrier of (S)) Element of bool [: the carrier of (S), the carrier of (S):]
[: the carrier of (S), the carrier of (S):] is non empty set
bool [: the carrier of (S), the carrier of (S):] is non empty set
[T,A1] is set
{T,A1} is non empty set
{T} is non empty trivial V49(1) set
{{T,A1},{T}} is non empty set
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
((bool S)) is non empty strict V84() reflexive transitive antisymmetric RelStr
((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]
[:(bool S),(bool S):] is non empty set
bool [:(bool S),(bool S):] is non empty set
RelStr(# (bool S),((bool S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued reflexive antisymmetric transitive V34( the carrier of (S)) Element of bool [: the carrier of (S), the carrier of (S):]
[: the carrier of (S), the carrier of (S):] is non empty set
bool [: the carrier of (S), the carrier of (S):] is non empty set
A1 is Relation-like bool S -defined bool S -valued Element of bool [:(bool S),(bool S):]
A2 is set
a is Element of the carrier of (S)
f is Element of the carrier of (S)
[A2,f] is set
{A2,f} is non empty set
{A2} is non empty trivial V49(1) set
{{A2,f},{A2}} is non empty set
dom A1 is Element of bool (bool S)
bool (bool S) is non empty set
A2 is set
a is set
[A2,a] is set
{A2,a} is non empty set
{A2} is non empty trivial V49(1) set
{{A2,a},{A2}} is non empty set
f is Element of the carrier of (S)
x9 is Element of the carrier of (S)
f is Element of the carrier of (S)
x9 is Element of the carrier of (S)
A2 is set
a is Element of the carrier of (S)
f is Element of the carrier of (S)
[f,A2] is set
{f,A2} is non empty set
{f} is non empty trivial V49(1) set
{{f,A2},{f}} is non empty set
field the InternalRel of (S) is set
dom the InternalRel of (S) is set
rng the InternalRel of (S) is set
(dom the InternalRel of (S)) \/ (rng the InternalRel of (S)) is set
(bool S) \/ (bool S) is non empty Element of bool (bool S)
S is set
bool S is non empty set
bool (bool S) is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
A1 is Element of bool (bool S)
(A1) is strict V84() reflexive transitive antisymmetric RelStr
(A1) is Relation-like A1 -defined A1 -valued reflexive antisymmetric transitive V34(A1) Element of bool [:A1,A1:]
[:A1,A1:] is set
bool [:A1,A1:] is non empty set
RelStr(# A1,(A1) #) is strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
bool the carrier of (S) is non empty set
bool S is non empty Element of bool (bool S)
[:(bool S),(bool S):] is non empty set
bool [:(bool S),(bool S):] is non empty set
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued reflexive antisymmetric transitive V34( the carrier of (S)) Element of bool [: the carrier of (S), the carrier of (S):]
[: the carrier of (S), the carrier of (S):] is non empty set
bool [: the carrier of (S), the carrier of (S):] is non empty set
a is Relation-like bool S -defined bool S -valued Element of bool [:(bool S),(bool S):]
f is set
x9 is Element of the carrier of (S)
f is Element of the carrier of (S)
[f,f] is set
{f,f} is non empty set
{f} is non empty trivial V49(1) set
{{f,f},{f}} is non empty set
dom a is Element of bool (bool S)
bool (bool S) is non empty set
f is set
x9 is set
[f,x9] is set
{f,x9} is non empty set
{f} is non empty trivial V49(1) set
{{f,x9},{f}} is non empty set
f is Element of the carrier of (S)
z is Element of the carrier of (S)
f is Element of the carrier of (S)
z is Element of the carrier of (S)
f is set
x9 is Element of the carrier of (S)
f is Element of the carrier of (S)
[f,f] is set
{f,f} is non empty set
{f} is non empty trivial V49(1) set
{{f,f},{f}} is non empty set
field the InternalRel of (S) is set
dom the InternalRel of (S) is set
rng the InternalRel of (S) is set
(dom the InternalRel of (S)) \/ (rng the InternalRel of (S)) is set
(bool S) \/ (bool S) is non empty Element of bool (bool S)
((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]
A2 is Element of bool the carrier of (S)
the InternalRel of (S) |_2 A2 is Relation-like A2 -defined A2 -valued Element of bool [:A2,A2:]
[:A2,A2:] is set
bool [:A2,A2:] is non empty set
RelStr(# A2,( the InternalRel of (S) |_2 A2) #) is strict RelStr
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
T \/ A1 is set
T "\/" A1 is Element of the carrier of (S)
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
T "/\" A1 is Element of the carrier of (S)
T /\ A1 is set
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
T \/ A1 is set
T "\/" A1 is Element of the carrier of (S)
A2 is Element of the carrier of (S)
a is Element of the carrier of (S)
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
T /\ A1 is set
T "/\" A1 is Element of the carrier of (S)
A2 is Element of the carrier of (S)
a is Element of the carrier of (S)
S is RelStr
the carrier of S is set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is non empty set
( the carrier of S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
T is set
A1 is set
[T,A1] is set
{T,A1} is non empty set
{T} is non empty trivial V49(1) set
{{T,A1},{T}} is non empty set
A2 is Element of the carrier of S
a is Element of the carrier of S
A2 is Element of the carrier of S
a is Element of the carrier of S
T is set
A1 is Element of the carrier of S
A2 is Element of the carrier of S
[T,A2] is set
{T,A2} is non empty set
{T} is non empty trivial V49(1) set
{{T,A2},{T}} is non empty set
dom the InternalRel of S is Element of bool the carrier of S
bool the carrier of S is non empty set
T is set
A1 is Element of the carrier of S
A2 is Element of the carrier of S
[A2,T] is set
{A2,T} is non empty set
{A2} is non empty trivial V49(1) set
{{A2,T},{A2}} is non empty set
field the InternalRel of S is set
dom the InternalRel of S is set
rng the InternalRel of S is set
(dom the InternalRel of S) \/ (rng the InternalRel of S) is set
the carrier of S \/ the carrier of S is set
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
A1 is Element of the carrier of (S)
A2 is Element of the carrier of (S)
{A1,A2} is non empty set
A1 "\/" A2 is Element of the carrier of (S)
a is Element of the carrier of (S)
A1 \/ A2 is set
f is Element of the carrier of (S)
a is Element of the carrier of (S)
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
A1 is Element of the carrier of (S)
A2 is Element of the carrier of (S)
{A1,A2} is non empty set
A1 "/\" A2 is Element of the carrier of (S)
a is Element of the carrier of (S)
A1 /\ A2 is set
f is Element of the carrier of (S)
a is Element of the carrier of (S)
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Bottom (S) is Element of the carrier of (S)
the carrier of (S) is non empty set
A1 is Element of the carrier of (S)
T is Element of the carrier of (S)
"\/" ({},(S)) is Element of the carrier of (S)
S is non empty set
union S is set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Top (S) is Element of the carrier of (S)
the carrier of (S) is non empty set
A1 is Element of the carrier of (S)
T is Element of the carrier of (S)
"/\" ({},(S)) is Element of the carrier of (S)
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
union S is set
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is set
A2 is set
a is Element of the carrier of (S)
S is non empty set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr
(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
meet S is set
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is set
A2 is set
a is Element of the carrier of (S)
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
T /\ A1 is set
T \/ A1 is set
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
A1 is Element of the carrier of (S)
T "\/" A1 is Element of the carrier of (S)
T \/ A1 is set
T "/\" A1 is Element of the carrier of (S)
T /\ A1 is set
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
((bool S)) is non empty strict V84() reflexive transitive antisymmetric RelStr
((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]
[:(bool S),(bool S):] is non empty set
bool [:(bool S),(bool S):] is non empty set
RelStr(# (bool S),((bool S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of ((bool S)) is non empty set
A2 is Element of the carrier of ((bool S))
a is Element of the carrier of ((bool S))
A2 "/\" a is Element of the carrier of ((bool S))
A2 /\ a is set
A2 "\/" a is Element of the carrier of ((bool S))
A2 \/ a is set
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Bottom (S) is Element of the carrier of (S)
the carrier of (S) is non empty set
"\/" ({},(LattPOSet (BooleLatt S))) is Element of the carrier of (LattPOSet (BooleLatt S))
the carrier of (LattPOSet (BooleLatt S)) is non empty set
"\/" ({},(BooleLatt S)) is Element of the carrier of (BooleLatt S)
Bottom (BooleLatt S) is Element of the carrier of (BooleLatt S)
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Top (S) is Element of the carrier of (S)
the carrier of (S) is non empty set
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
((bool S)) is non empty strict V84() reflexive transitive antisymmetric RelStr
((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]
[:(bool S),(bool S):] is non empty set
bool [:(bool S),(bool S):] is non empty set
RelStr(# (bool S),((bool S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Top ((bool S)) is Element of the carrier of ((bool S))
the carrier of ((bool S)) is non empty set
union (bool S) is Element of bool S
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
bool the carrier of (S) is non empty set
A1 is non empty Element of bool the carrier of (S)
"/\" (A1,(S)) is Element of the carrier of (S)
meet A1 is set
the Element of A1 is Element of A1
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
f is Element of the carrier of (S)
x9 is set
f is Element of the carrier of (S)
a is Element of the carrier of (S)
f is Element of the carrier of (S)
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr
LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
the carrier of (BooleLatt S) is non empty set
K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]
[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set
RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of (S) is non empty set
bool the carrier of (S) is non empty set
A1 is Element of bool the carrier of (S)
"\/" (A1,(S)) is Element of the carrier of (S)
union A1 is set
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
union (bool S) is Element of bool S
a is Element of the carrier of (S)
f is set
x9 is Element of the carrier of (S)
A2 is Element of the carrier of (S)
a is Element of the carrier of (S)
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of ( the topology of S) is non empty set
bool the carrier of ( the topology of S) is non empty set
A1 is Element of bool the carrier of ( the topology of S)
"\/" (A1,( the topology of S)) is Element of the carrier of ( the topology of S)
union A1 is set
A2 is Element of bool (bool the carrier of S)
union A2 is Element of bool the carrier of S
f is Element of the carrier of ( the topology of S)
x9 is set
f is Element of the carrier of ( the topology of S)
a is Element of the carrier of ( the topology of S)
f is Element of the carrier of ( the topology of S)
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Bottom ( the topology of S) is Element of the carrier of ( the topology of S)
the carrier of ( the topology of S) is non empty set
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of ( the topology of S) is non empty set
A1 is Element of the carrier of ( the topology of S)
A2 is Element of the carrier of ( the topology of S)
a is Element of the carrier of ( the topology of S)
A2 is Element of the carrier of ( the topology of S)
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
Top ( the topology of S) is Element of the carrier of ( the topology of S)
the carrier of ( the topology of S) is non empty set
"/\" ({},( the topology of S)) is Element of the carrier of ( the topology of S)
A2 is Element of the carrier of ( the topology of S)
a is Element of the carrier of ( the topology of S)
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
A1 is V84() reflexive transitive antisymmetric lower-bounded RelStr
the carrier of A1 is set
bool the carrier of A1 is non empty set
A2 is Element of bool the carrier of A1
union A2 is set
f is Element of bool (bool the carrier of S)
the carrier of ( the topology of S) is non empty set
x9 is Element of the carrier of ( the topology of S)
f is Element of the carrier of ( the topology of S)
z is set
x1 is Element of the carrier of ( the topology of S)
f is Element of the carrier of ( the topology of S)
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of ( the topology of S) is non empty set
A1 is Element of the carrier of ( the topology of S)
A2 is Element of the carrier of ( the topology of S)
S is non empty TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
the topology of S is non empty Element of bool (bool the carrier of S)
( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr
( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
the carrier of ( the topology of S) is non empty set
bool the carrier of ( the topology of S) is non empty set
T is Element of bool (bool the carrier of S)
A1 is set
A2 is Element of bool the carrier of S
A1 is Element of bool the carrier of S
S is Relation-like Function-like set
T is set
dom S is set
S . T is set
rng S is set
S is set
the RelStr is RelStr
S --> the RelStr is Relation-like S -defined { the RelStr } -valued Function-like constant V34(S) quasi_total Element of bool [:S,{ the RelStr }:]
{ the RelStr } is non empty trivial V49(1) set
[:S,{ the RelStr }:] is set
bool [:S,{ the RelStr }:] is non empty set
A1 is set
rng (S --> the RelStr ) is set
S is non empty set
T is Relation-like S -defined Function-like V34(S) 1-sorted-yielding () set
A1 is Element of S
T . A1 is set
dom T is Element of bool S
bool S is non empty set
T . A1 is 1-sorted
rng T is set
S is set
T is Relation-like S -defined Function-like V34(S) 1-sorted-yielding () set
Carrier T is Relation-like S -defined Function-like V34(S) set
product (Carrier T) is set
[:(product (Carrier T)),(product (Carrier T)):] is set
bool [:(product (Carrier T)),(product (Carrier T)):] is non empty set
A1 is Relation-like product (Carrier T) -defined product (Carrier T) -valued Element of bool [:(product (Carrier T)),(product (Carrier T)):]
RelStr(# (product (Carrier T)),A1 #) is strict RelStr
A2 is strict RelStr
the carrier of A2 is set
a is Element of the carrier of A2
f is Element of the carrier of A2
[a,f] is set
{a,f} is non empty set
{a} is non empty trivial V49(1) set
{{a,f},{a}} is non empty set
the InternalRel of A2 is Relation-like the carrier of A2 -defined the carrier of A2 -valued Element of bool [: the carrier of A2, the carrier of A2:]
[: the carrier of A2, the carrier of A2:] is set
bool [: the carrier of A2, the carrier of A2:] is non empty set
x9 is Relation-like Function-like set
f is Relation-like Function-like set
A1 is strict RelStr
the carrier of A1 is set
A2 is strict RelStr
the carrier of A2 is set
the InternalRel of A1 is Relation-like the carrier of A1 -defined the carrier of A1 -valued Element of bool [: the carrier of A1, the carrier of A1:]
[: the carrier of A1, the carrier of A1:] is set
bool [: the carrier of A1, the carrier of A1:] is non empty set
the InternalRel of A2 is Relation-like the carrier of A2 -defined the carrier of A2 -valued Element of bool [: the carrier of A2, the carrier of A2:]
[: the carrier of A2, the carrier of A2:] is set
bool [: the carrier of A2, the carrier of A2:] is non empty set
a is set
f is set
[a,f] is set
{a,f} is non empty set
{a} is non empty trivial V49(1) set
{{a,f},{a}} is non empty set
x9 is Element of the carrier of A1
f is Element of the carrier of A1
z is Element of the carrier of A2
x1 is Element of the carrier of A2
z1 is Relation-like Function-like set
i is Relation-like Function-like set
x9 is Element of the carrier of A2
f is Element of the carrier of A2
z is Element of the carrier of A1
x1 is Element of the carrier of A1
z1 is Relation-like Function-like set
i is Relation-like Function-like set
S is set
T is RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
A1 is set
rng (S --> T) is set
S is set
T is RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
id {{}} is non empty Relation-like {{}} -defined {{}} -valued reflexive symmetric antisymmetric transitive V34({{}}) Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is non empty set
bool [:{{}},{{}}:] is non empty set
RelStr(# {{}},(id {{}}) #) is non empty trivial V57() 1 -element strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
S is Relation-like {} -defined Function-like V34( {} ) 1-sorted-yielding () set
({},S) is strict RelStr
the carrier of ({},S) is set
Carrier S is Relation-like {} -defined Function-like V34( {} ) set
product (Carrier S) is set
the InternalRel of ({},S) is Relation-like the carrier of ({},S) -defined the carrier of ({},S) -valued Element of bool [: the carrier of ({},S), the carrier of ({},S):]
[: the carrier of ({},S), the carrier of ({},S):] is set
bool [: the carrier of ({},S), the carrier of ({},S):] is non empty set
a is set
f is set
[a,f] is set
{a,f} is non empty set
{a} is non empty trivial V49(1) set
{{a,f},{a}} is non empty set
A1 is Element of the carrier of ({},S)
{} --> {{}} is empty Relation-like non-empty {} -defined {{{}}} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() Element of bool [:{},{{{}}}:]
{{{}}} is non empty trivial V49(1) set
[:{},{{{}}}:] is set
bool [:{},{{{}}}:] is non empty set
A2 is Element of the carrier of ({},S)
x9 is Relation-like Function-like set
f is Relation-like Function-like set
z is set
S . z is set
x9 . z is set
f . z is set
S is RelStr
({},S) is strict RelStr
{} --> S is empty Relation-like {} -defined {S} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() 1-sorted-yielding () Element of bool [:{},{S}:]
{S} is non empty trivial V49(1) set
[:{},{S}:] is set
bool [:{},{S}:] is non empty set
({},({} --> S)) is strict RelStr
S is set
T is RelStr
the carrier of T is set
Funcs (S, the carrier of T) is set
(S,T) is strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of (S,T) is set
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
dom (Carrier (S --> T)) is Element of bool S
bool S is non empty set
a is set
(Carrier (S --> T)) . a is set
(S --> T) . a is set
f is 1-sorted
the carrier of f is set
product (Carrier (S --> T)) is set
a is set
f is Relation-like Function-like set
dom f is set
rng f is set
x9 is set
(Carrier (S --> T)) . x9 is set
f . x9 is set
a is set
f is Relation-like Function-like set
dom f is set
rng f is set
x9 is set
f is set
f . f is set
(Carrier (S --> T)) . f is set
S is set
T is non empty RelStr
(S,T) is strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of T is non empty set
[:S, the carrier of T:] is set
bool [:S, the carrier of T:] is non empty set
the Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:] is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T
S is set
T is non empty RelStr
(S,T) is non empty strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of (S,T) is non empty set
the carrier of (S,(S --> T)) is set
the carrier of T is non empty set
[:S, the carrier of T:] is set
bool [:S, the carrier of T:] is non empty set
A1 is Element of the carrier of (S,T)
Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T
S is set
T is non empty V84() reflexive RelStr
(S,T) is non empty strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
A1 is non empty set
(A1,T) is non empty strict RelStr
A1 --> T is non empty Relation-like A1 -defined {T} -valued Function-like constant V34(A1) quasi_total 1-sorted-yielding () Element of bool [:A1,{T}:]
[:A1,{T}:] is non empty set
bool [:A1,{T}:] is non empty set
(A1,(A1 --> T)) is strict RelStr
the carrier of (A1,T) is non empty set
A2 is Element of the carrier of (A1,T)
the carrier of T is non empty set
[:A1, the carrier of T:] is non empty set
bool [:A1, the carrier of T:] is non empty set
the carrier of (A1,(A1 --> T)) is set
f is Element of the carrier of (A1,(A1 --> T))
a is Relation-like A1 -defined the carrier of T -valued Function-like quasi_total Element of bool [:A1, the carrier of T:]
x9 is set
(A1 --> T) . x9 is set
a . x9 is set
f is Element of A1
(A1,(A1 --> T),f) is RelStr
z is RelStr
the carrier of z is set
a . f is Element of the carrier of T
x1 is Element of the carrier of z
z1 is Element of the carrier of z
i is Element of the carrier of T
i is Element of the carrier of T
Carrier (A1 --> T) is Relation-like A1 -defined Function-like V34(A1) set
product (Carrier (A1 --> T)) is set
x9 is Relation-like Function-like set
f is Relation-like Function-like set
S is non empty RelStr
({},S) is non empty strict RelStr
{} --> S is empty Relation-like {} -defined {S} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() 1-sorted-yielding () Element of bool [:{},{S}:]
{S} is non empty trivial V49(1) set
[:{},{S}:] is set
bool [:{},{S}:] is non empty set
({},({} --> S)) is strict RelStr
S is non empty V84() reflexive RelStr
({},S) is non empty trivial V57() 1 -element strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr
{} --> S is empty Relation-like {} -defined {S} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() 1-sorted-yielding () Element of bool [:{},{S}:]
{S} is non empty trivial V49(1) set
[:{},{S}:] is set
bool [:{},{S}:] is non empty set
({},({} --> S)) is strict RelStr
S is set
T is non empty transitive RelStr
(S,T) is non empty strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of (S,T) is non empty set
the carrier of (S,(S --> T)) is set
A2 is Element of the carrier of (S,T)
a is Element of the carrier of (S,T)
f is Element of the carrier of (S,T)
f is Element of the carrier of (S,(S --> T))
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
z is Element of the carrier of (S,(S --> T))
x1 is Relation-like Function-like set
z1 is Relation-like Function-like set
x9 is Element of the carrier of (S,(S --> T))
i is Relation-like Function-like set
i is Relation-like Function-like set
the carrier of T is non empty set
[:S, the carrier of T:] is set
bool [:S, the carrier of T:] is non empty set
R is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
yi is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
xi is set
(S --> T) . xi is set
R . xi is set
yi . xi is set
c₁₇ is non empty set
c₁₇ --> T is non empty Relation-like c₁₇ -defined {T} -valued Function-like constant V34(c₁₇) quasi_total 1-sorted-yielding () Element of bool [:c₁₇,{T}:]
[:c₁₇,{T}:] is non empty set
bool [:c₁₇,{T}:] is non empty set
J is Element of c₁₇
(c₁₇,(c₁₇ --> T),J) is RelStr
f1 is RelStr
the carrier of f1 is set
R . J is set
yi . J is set
g1 is Element of the carrier of f1
i is Element of the carrier of f1
i . J is set
i . J is set
x1 . J is set
z1 . J is set
i is RelStr
the carrier of i is set
xi is RelStr
the carrier of xi is set
R is Element of the carrier of i
yi is Element of the carrier of i
c₂₆ is Element of the carrier of xi
c₂₇ is Element of the carrier of xi
R is Relation-like Function-like set
yi is Relation-like Function-like set
S is set
T is non empty antisymmetric RelStr
(S,T) is non empty strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of (S,T) is non empty set
the carrier of T is non empty set
[:S, the carrier of T:] is set
bool [:S, the carrier of T:] is non empty set
A2 is Element of the carrier of (S,T)
a is Element of the carrier of (S,T)
the carrier of (S,(S --> T)) is set
z is Element of the carrier of (S,(S --> T))
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
f is Element of the carrier of (S,(S --> T))
x1 is Relation-like Function-like set
z1 is Relation-like Function-like set
i is Relation-like Function-like set
i is Relation-like Function-like set
R is set
(S --> T) . R is set
x1 . R is set
z1 . R is set
yi is RelStr
the carrier of yi is set
xi is Element of the carrier of yi
c₁₇ is Element of the carrier of yi
i . R is set
i . R is set
J is RelStr
the carrier of J is set
f1 is Element of the carrier of J
g1 is Element of the carrier of J
f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
f . R is set
x9 is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
x9 . R is set
dom f is Element of bool S
bool S is non empty set
dom x9 is Element of bool S
S is non empty set
T is non empty antisymmetric with_infima RelStr
(S,T) is non empty strict antisymmetric RelStr
S --> T is non empty Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is non empty set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of (S,T) is non empty set
A2 is Element of the carrier of (S,T)
a is Element of the carrier of (S,T)
the carrier of T is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
x9 is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
f is set
x9 . f is set
f . f is set
z is Element of the carrier of T
x1 is Element of the carrier of T
z "/\" x1 is Element of the carrier of T
z1 is Element of the carrier of T
f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T
z is Element of the carrier of (S,T)
the carrier of (S,(S --> T)) is set
z1 is Element of the carrier of (S,(S --> T))
x1 is Element of the carrier of (S,(S --> T))
i is set
(S --> T) . i is set
f . i is set
f . i is set
i is Element of S
(S,(S --> T),i) is RelStr
R is RelStr
the carrier of R is set
f . i is Element of the carrier of T
f . i is Element of the carrier of T
yi is Element of the carrier of R
xi is Element of the carrier of R
x9 . i is Element of the carrier of T
c₁₇ is Element of the carrier of T
J is Element of the carrier of T
c₁₇ "/\" J is Element of the carrier of T
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
i is Relation-like Function-like set
i is Relation-like Function-like set
x1 is Element of the carrier of (S,T)
the carrier of (S,(S --> T)) is set
z1 is Element of the carrier of (S,(S --> T))
i is Element of the carrier of (S,(S --> T))
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
R is Element of the carrier of (S,(S --> T))
c₁₇ is Relation-like Function-like set
J is Relation-like Function-like set
i is Element of the carrier of (S,(S --> T))
f1 is Relation-like Function-like set
g1 is Relation-like Function-like set
yi is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
xi is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
i is set
(S --> T) . i is set
yi . i is set
xi . i is set
i is Element of S
(S,(S --> T),i) is RelStr
R is RelStr
the carrier of R is set
yi . i is Element of the carrier of T
xi . i is Element of the carrier of T
yi is Element of the carrier of R
xi is Element of the carrier of R
x9 . i is Element of the carrier of T
f . i is Element of the carrier of T
f . i is Element of the carrier of T
c₁₇ . i is set
J . i is set
f1 . i is set
g1 . i is set
c₂₆ is RelStr
the carrier of c₂₆ is set
c₂₉ is RelStr
the carrier of c₂₉ is set
c₂₇ is Element of the carrier of c₂₆
c₂₈ is Element of the carrier of c₂₆
c₃₀ is Element of the carrier of c₂₉
c₃₁ is Element of the carrier of c₂₉
c₃₂ is Element of the carrier of T
c₃₃ is Element of the carrier of T
c₃₂ "/\" c₃₃ is Element of the carrier of T
i is Relation-like Function-like set
i is Relation-like Function-like set
the carrier of (S,(S --> T)) is set
z1 is Element of the carrier of (S,(S --> T))
x1 is Element of the carrier of (S,(S --> T))
i is set
(S --> T) . i is set
f . i is set
x9 . i is set
i is Element of S
(S,(S --> T),i) is RelStr
R is RelStr
the carrier of R is set
f . i is Element of the carrier of T
x9 . i is Element of the carrier of T
yi is Element of the carrier of R
xi is Element of the carrier of R
f . i is Element of the carrier of T
c₁₇ is Element of the carrier of T
J is Element of the carrier of T
c₁₇ "/\" J is Element of the carrier of T
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
i is Relation-like Function-like set
i is Relation-like Function-like set
x1 is Element of the carrier of (S,T)
S is non empty set
T is non empty antisymmetric with_suprema RelStr
(S,T) is non empty strict antisymmetric RelStr
S --> T is non empty Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]
{T} is non empty trivial V49(1) set
[:S,{T}:] is non empty set
bool [:S,{T}:] is non empty set
(S,(S --> T)) is strict RelStr
the carrier of (S,T) is non empty set
A2 is Element of the carrier of (S,T)
a is Element of the carrier of (S,T)
the carrier of T is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
x9 is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
f is set
x9 . f is set
f . f is set
z is Element of the carrier of T
x1 is Element of the carrier of T
z "\/" x1 is Element of the carrier of T
z1 is Element of the carrier of T
f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T
z is Element of the carrier of (S,T)
the carrier of (S,(S --> T)) is set
x1 is Element of the carrier of (S,(S --> T))
z1 is Element of the carrier of (S,(S --> T))
i is set
(S --> T) . i is set
f . i is set
f . i is set
i is Element of S
(S,(S --> T),i) is RelStr
R is RelStr
the carrier of R is set
f . i is Element of the carrier of T
f . i is Element of the carrier of T
xi is Element of the carrier of R
yi is Element of the carrier of R
x9 . i is Element of the carrier of T
c₁₇ is Element of the carrier of T
J is Element of the carrier of T
c₁₇ "\/" J is Element of the carrier of T
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
i is Relation-like Function-like set
i is Relation-like Function-like set
x1 is Element of the carrier of (S,T)
the carrier of (S,(S --> T)) is set
i is Element of the carrier of (S,(S --> T))
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
z1 is Element of the carrier of (S,(S --> T))
yi is Relation-like Function-like set
xi is Relation-like Function-like set
i is Element of the carrier of (S,(S --> T))
R is Element of the carrier of (S,(S --> T))
f1 is Relation-like Function-like set
g1 is Relation-like Function-like set
c₁₇ is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
J is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]
i is set
(S --> T) . i is set
c₁₇ . i is set
J . i is set
i is Element of S
(S,(S --> T),i) is RelStr
R is RelStr
the carrier of R is set
J . i is Element of the carrier of T
c₁₇ . i is Element of the carrier of T
xi is Element of the carrier of R
yi is Element of the carrier of R
x9 . i is Element of the carrier of T
f . i is Element of the carrier of T
f . i is Element of the carrier of T
f1 . i is set
g1 . i is set
yi . i is set
xi . i is set
c₂₆ is RelStr
the carrier of c₂₆ is set
c₂₉ is RelStr
the carrier of c₂₉ is set
c₂₇ is Element of the carrier of c₂₆
c₂₈ is Element of the carrier of c₂₆
c₃₀ is Element of the carrier of c₂₉
c₃₁ is Element of the carrier of c₂₉
c₃₂ is Element of the carrier of T
c₃₃ is Element of the carrier of T
c₃₂ "\/" c₃₃ is Element of the carrier of T
i is Relation-like Function-like set
i is Relation-like Function-like set
the carrier of (S,(S --> T)) is set
x1 is Element of the carrier of (S,(S --> T))
z1 is Element of the carrier of (S,(S --> T))
i is set
(S --> T) . i is set
x9 . i is set
f . i is set
i is Element of S
(S,(S --> T),i) is RelStr
R is RelStr
the carrier of R is set
f . i is Element of the carrier of T
x9 . i is Element of the carrier of T
xi is Element of the carrier of R
yi is Element of the carrier of R
f . i is Element of the carrier of T
c₁₇ is Element of the carrier of T
J is Element of the carrier of T
c₁₇ "\/" J is Element of the carrier of T
Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set
product (Carrier (S --> T)) is set
i is Relation-like Function-like set
i is Relation-like Function-like set
x1 is Element of the carrier of (S,T)
S is RelStr
the carrier of S is set
T is RelStr
( the carrier of S,T) is strict RelStr
the carrier of S --> T is Relation-like the carrier of S -defined {T} -valued Function-like constant V34( the carrier of S) quasi_total 1-sorted-yielding () Element of bool [: the carrier of S,{T}:]
{T} is non empty trivial V49(1) set
[: the carrier of S,{T}:] is set
bool [: the carrier of S,{T}:] is non empty set
( the carrier of S,( the carrier of S --> T)) is strict RelStr
the carrier of T is set
[: the carrier of S, the carrier of T:] is set
bool [: the carrier of S, the carrier of T:] is non empty set
Funcs ( the carrier of S, the carrier of T) is set
MonFuncs (S,T) is set
the carrier of ( the carrier of S,T) is set
bool the carrier of ( the carrier of S,T) is non empty set
A2 is Element of bool the carrier of ( the carrier of S,T)
subrelstr A2 is strict full SubRelStr of ( the carrier of S,T)
a is strict full SubRelStr of ( the carrier of S,T)
the carrier of a is set
f is Relation-like the carrier of S -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of T:]
x9 is Relation-like the carrier of S -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of T:]
A1 is strict full SubRelStr of ( the carrier of S,T)
the carrier of A1 is set
A2 is strict full SubRelStr of ( the carrier of S,T)
the carrier of A2 is set
the carrier of ( the carrier of S,T) is set
a is set
f is Relation-like the carrier of S -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is set
f is Relation-like the carrier of S -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of T:]