:: 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()
is set
bool is non empty set
K58(K245(),) is non empty functional set
{{},1} is non empty set

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 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 () is non empty set
Top () is Element of the carrier of ()
T is Element of the carrier of ()
A1 is Element of the carrier of S
Top S is Element of the carrier of S
a is Element of the carrier of ()
f is Element of the carrier of S
f % is Element of the carrier of ()
A1 % is Element of the carrier of ()
A2 is Element of the carrier of ()
"/\" ({},()) is Element of the carrier of ()
f is Element of the carrier of ()
x9 is Element of the carrier of S
a is Element of the carrier of S
x9 % is Element of the carrier of ()
a % is Element of the carrier of ()
T is Element of the carrier of ()

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 () is non empty set
Bottom () is Element of the carrier of ()
T is Element of the carrier of ()
A1 is Element of the carrier of S
Bottom S is Element of the carrier of S
a is Element of the carrier of ()
f is Element of the carrier of S
f % is Element of the carrier of ()
A1 % is Element of the carrier of ()
A2 is Element of the carrier of ()
"\/" ({},()) is Element of the carrier of ()
f is Element of the carrier of ()
a is Element of the carrier of S
x9 is Element of the carrier of S
x9 % is Element of the carrier of ()
a % is Element of the carrier of ()
T is Element of the carrier of ()

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 () is non empty set
T is set
"\/" (T,()) is Element of the carrier of ()
A1 is Element of the carrier of ()
"\/" (T,S) is Element of the carrier of S
("\/" (T,S)) % is Element of the carrier of ()
A2 is Element of the carrier of ()
a is Element of the carrier of S
a % is Element of the carrier of ()
S is 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 () is set
dom () is set
rng () is set
(dom ()) \/ (rng ()) is set

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,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,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 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,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,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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is strict RelStr

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set
(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
S is set

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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 ()
A2 % is Element of the carrier of ()
the carrier of () is non empty set
a is Element of the carrier of ()
a % is Element of the carrier of ()
A2 is Element of the carrier of ()
a is Element of the carrier of ()
A2 % is Element of the carrier of ()
the carrier of () is non empty set
a % is Element of the carrier of ()
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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) is non empty strict V84() reflexive transitive antisymmetric RelStr
A1 is Element of bool (bool S)

(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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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
"\/" ({},()) is Element of the carrier of ()
the carrier of () is non empty set
"\/" ({},()) is Element of the carrier of ()
Bottom () is Element of the carrier of ()
S is set

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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

the carrier of () is non empty set
K167(()) is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V34( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),K167(()) #) 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

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

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

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

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

product () is set
[:(product ()),(product ()):] is set
bool [:(product ()),(product ()):] is non empty set
A1 is Relation-like product () -defined product () -valued Element of bool [:(product ()),(product ()):]
RelStr(# (product ()),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

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

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

S is set
T is RelStr

{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

{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

is non empty set
bool is non empty set

({},S) is strict RelStr
the carrier of ({},S) is set

product () 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 non empty trivial V49(1) set

bool is non empty set
A2 is Element of the carrier of ({},S)

z is set
S . z is set
x9 . z is set
f . z is set
S is RelStr
({},S) is strict RelStr

{S} is non empty trivial V49(1) set
[:{},{S}:] is set
bool [:{},{S}:] is non empty set
({},()) 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

{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

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

dom f is set
rng f is set
x9 is set
(Carrier (S --> T)) . x9 is set
f . x9 is set
a is 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

{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

{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

{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 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

S is non empty RelStr
({},S) is non empty strict RelStr

{S} is non empty trivial V49(1) set
[:{},{S}:] is set
bool [:{},{S}:] is non empty set
({},()) is strict RelStr
S is non empty V84() reflexive RelStr

{S} is non empty trivial V49(1) set
[:{},{S}:] is set
bool [:{},{S}:] is non empty set
({},()) is strict RelStr
S is set
T is non empty transitive RelStr
(S,T) is non empty strict RelStr

{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))

product (Carrier (S --> T)) is set
z is Element of the carrier of (S,(S --> T))

x9 is Element of the carrier of (S,(S --> T))

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
c17 is non empty set
c17 --> T is non empty Relation-like c17 -defined {T} -valued Function-like constant V34(c17) quasi_total 1-sorted-yielding () Element of bool [:c17,{T}:]
[:c17,{T}:] is non empty set
bool [:c17,{T}:] is non empty set
J is Element of c17
(c17,(c17 --> 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
c26 is Element of the carrier of xi
c27 is Element of the carrier of xi

S is set
T is non empty antisymmetric RelStr
(S,T) is non empty strict RelStr

{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))

product (Carrier (S --> T)) is set
f is Element of the carrier of (S,(S --> T))

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
c17 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

{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
c17 is Element of the carrier of T
J is Element of the carrier of T
c17 "/\" J is Element of the carrier of T

product (Carrier (S --> T)) is 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))

product (Carrier (S --> T)) is set
R is Element of the carrier of (S,(S --> T))

i is Element of the carrier of (S,(S --> 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 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
c17 . i is set
J . i is set
f1 . i is set
g1 . i is set
c26 is RelStr
the carrier of c26 is set
c29 is RelStr
the carrier of c29 is set
c27 is Element of the carrier of c26
c28 is Element of the carrier of c26
c30 is Element of the carrier of c29
c31 is Element of the carrier of c29
c32 is Element of the carrier of T
c33 is Element of the carrier of T
c32 "/\" c33 is Element of the carrier of 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
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
c17 is Element of the carrier of T
J is Element of the carrier of T
c17 "/\" J is Element of the carrier of T

product (Carrier (S --> T)) is 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

{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
c17 is Element of the carrier of T
J is Element of the carrier of T
c17 "\/" J is Element of the carrier of T

product (Carrier (S --> T)) is 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))

product (Carrier (S --> T)) is set
z1 is Element of the carrier of (S,(S --> T))

i is Element of the carrier of (S,(S --> T))
R is Element of the carrier of (S,(S --> T))

c17 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
c17 . 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
c17 . 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
c26 is RelStr
the carrier of c26 is set
c29 is RelStr
the carrier of c29 is set
c27 is Element of