:: WAYBEL29 semantic presentation

K99() is Element of bool K95()
K95() is set
bool K95() is non empty set
K54() is set
bool K54() is non empty set
bool K99() is non empty set
K246() is non empty strict TopSpace-like TopStruct
the carrier of K246() is non empty set
K96() is set
K97() is set
K98() is set
[:K95(),K95():] is set
bool [:K95(),K95():] is non empty set
K409() is non empty V119() L9()
the carrier of K409() is non empty set
K414() is non empty L9()
K415() is non empty V119() M22(K414())
K416() is non empty V119() V141() V201() M25(K414(),K415())
K418() is non empty V119() V141() V143() V145() L9()
K419() is non empty V119() V141() V201() M22(K418())
{} is set

1 is non empty set
{{},1} is finite set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
K652() is set

K380() is M19()
is set
bool is non empty set
K39(K380(),) is set

bool is non empty finite V45() set
RelStr(# ,() #) is non empty trivial finite 1 -element strict RelStr

0 is Element of K99()
{0,1} is finite set
{{},{1},{0,1}} is non empty finite set

the carrier of () is non empty set
L is non empty set
S is non empty set
[:L,S:] is non empty set
S is non empty RelStr
S |^ [:L,S:] is non empty V185() strict RelStr
S |^ S is non empty V185() strict RelStr
(S |^ S) |^ L is non empty V185() strict RelStr
SS is non empty V185() SubRelStr of S |^ [:L,S:]
the carrier of SS is functional non empty set
Wy is non empty V185() SubRelStr of (S |^ S) |^ L
the carrier of Wy is functional non empty set
[: the carrier of SS, the carrier of Wy:] is non empty set
bool [: the carrier of SS, the carrier of Wy:] is non empty set
T is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]
T " is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]
[: the carrier of Wy, the carrier of SS:] is non empty set
bool [: the carrier of Wy, the carrier of SS:] is non empty set
rng T is functional Element of bool the carrier of Wy
bool the carrier of Wy is non empty set

the carrier of (S |^ S) is functional non empty set
Funcs (L, the carrier of (S |^ S)) is functional non empty FUNCTION_DOMAIN of L, the carrier of (S |^ S)
the carrier of ((S |^ S) |^ L) is functional non empty set
the carrier of S is non empty set
Funcs (S, the carrier of S) is functional non empty FUNCTION_DOMAIN of S, the carrier of S
WY is set
dom (T ") is functional Element of bool the carrier of Wy
[:L,(Funcs (S, the carrier of S)):] is non empty set
bool [:L,(Funcs (S, the carrier of S)):] is non empty set
proj1 (T ") is set

(T ") . WY is Relation-like Function-like set

dom T is functional Element of bool the carrier of SS
bool the carrier of SS is non empty set
T1 is set

Funcs ([:L,S:], the carrier of S) is functional non empty FUNCTION_DOMAIN of [:L,S:], the carrier of S
the carrier of (S |^ [:L,S:]) is functional non empty set

[:[:L,S:], the carrier of S:] is non empty set
bool [:[:L,S:], the carrier of S:] is non empty set
proj1 wy is set

L is non empty set
S is non empty set
[:L,S:] is non empty set
S is non empty RelStr
S |^ [:L,S:] is non empty V185() strict RelStr
S |^ S is non empty V185() strict RelStr
(S |^ S) |^ L is non empty V185() strict RelStr
SS is non empty V185() SubRelStr of S |^ [:L,S:]
the carrier of SS is functional non empty set
Wy is non empty V185() SubRelStr of (S |^ S) |^ L
the carrier of Wy is functional non empty set
[: the carrier of Wy, the carrier of SS:] is non empty set
bool [: the carrier of Wy, the carrier of SS:] is non empty set
T is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]
T " is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]
[: the carrier of SS, the carrier of Wy:] is non empty set
bool [: the carrier of SS, the carrier of Wy:] is non empty set
the carrier of (S |^ S) is functional non empty set
Funcs (L, the carrier of (S |^ S)) is functional non empty FUNCTION_DOMAIN of L, the carrier of (S |^ S)
the carrier of ((S |^ S) |^ L) is functional non empty set
the carrier of S is non empty set
Funcs (S, the carrier of S) is functional non empty FUNCTION_DOMAIN of S, the carrier of S
rng T is functional Element of bool the carrier of SS
bool the carrier of SS is non empty set

Funcs ([:L,S:], the carrier of S) is functional non empty FUNCTION_DOMAIN of [:L,S:], the carrier of S
the carrier of (S |^ [:L,S:]) is functional non empty set
WY is set
dom (T ") is functional Element of bool the carrier of SS
[:[:L,S:], the carrier of S:] is non empty set
bool [:[:L,S:], the carrier of S:] is non empty set
T1 is Relation-like [:L,S:] -defined the carrier of S -valued Function-like non empty V24([:L,S:]) quasi_total Element of bool [:[:L,S:], the carrier of S:]

bool [:L,S:] is non empty set

proj1 WY is set
proj1 (T ") is set

(T ") . WY is Relation-like Function-like set

dom T is functional Element of bool the carrier of Wy
bool the carrier of Wy is non empty set
T1 is set

[:L,(Funcs (S, the carrier of S)):] is non empty set
bool [:L,(Funcs (S, the carrier of S)):] is non empty set
proj2 wy is set

L is non empty set
S is non empty set
[:L,S:] is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
S |^ [:L,S:] is non empty V185() strict reflexive transitive antisymmetric non void RelStr
S |^ S is non empty V185() strict reflexive transitive antisymmetric non void RelStr
(S |^ S) |^ L is non empty V185() strict reflexive transitive antisymmetric non void RelStr
SS is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of S |^ [:L,S:]
the carrier of SS is functional non empty set
Wy is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of (S |^ S) |^ L
the carrier of Wy is functional non empty set
[: the carrier of SS, the carrier of Wy:] is non empty set
bool [: the carrier of SS, the carrier of Wy:] is non empty set
T is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]
T " is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]
[: the carrier of Wy, the carrier of SS:] is non empty set
bool [: the carrier of Wy, the carrier of SS:] is non empty set
T * (T ") is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]
[: the carrier of Wy, the carrier of Wy:] is non empty set
bool [: the carrier of Wy, the carrier of Wy:] is non empty set

id the carrier of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like one-to-one non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]
(T ") * T is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]
[: the carrier of SS, the carrier of SS:] is non empty set
bool [: the carrier of SS, the carrier of SS:] is non empty set

id the carrier of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like one-to-one non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]
L is non empty set
S is non empty set
[:L,S:] is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
S |^ [:L,S:] is non empty V185() strict reflexive transitive antisymmetric non void RelStr
S |^ S is non empty V185() strict reflexive transitive antisymmetric non void RelStr
(S |^ S) |^ L is non empty V185() strict reflexive transitive antisymmetric non void RelStr
SS is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of S |^ [:L,S:]
the carrier of SS is functional non empty set
Wy is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of (S |^ S) |^ L
the carrier of Wy is functional non empty set
[: the carrier of Wy, the carrier of SS:] is non empty set
bool [: the carrier of Wy, the carrier of SS:] is non empty set
T is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]
T " is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]
[: the carrier of SS, the carrier of Wy:] is non empty set
bool [: the carrier of SS, the carrier of Wy:] is non empty set
T * (T ") is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]
[: the carrier of SS, the carrier of SS:] is non empty set
bool [: the carrier of SS, the carrier of SS:] is non empty set

id the carrier of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like one-to-one non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]
(T ") * T is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]
[: the carrier of Wy, the carrier of Wy:] is non empty set
bool [: the carrier of Wy, the carrier of Wy:] is non empty set

id the carrier of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like one-to-one non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]
L is RelStr
the carrier of L is set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
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
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
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
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
SS is RelStr
the carrier of SS is set
the InternalRel of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Element of bool [: the carrier of SS, the carrier of SS:]
[: the carrier of SS, the carrier of SS:] is set
bool [: the carrier of SS, the carrier of SS:] is non empty set
RelStr(# the carrier of SS, the InternalRel of SS #) is strict RelStr
[: the carrier of L, the carrier of S:] is set
bool [: the carrier of L, the carrier of S:] is non empty set
[: the carrier of S, the carrier of SS:] is set
bool [: the carrier of S, the carrier of SS:] is non empty set
Wy is Relation-like the carrier of L -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of S:]
T is Relation-like the carrier of S -defined the carrier of SS -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of SS:]
WY is non empty RelStr
the carrier of WY is non empty set
T1 is non empty RelStr
the carrier of T1 is non empty set
[: the carrier of WY, the carrier of T1:] is non empty set
bool [: the carrier of WY, the carrier of T1:] is non empty set
x is non empty RelStr
the carrier of x is non empty set
y is non empty RelStr
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty set
bool [: the carrier of x, the carrier of y:] is non empty set
x2 is Element of the carrier of x
u2 is Element of the carrier of x
u1 is Element of the carrier of WY
y1 is Element of the carrier of WY
x1 is Relation-like the carrier of x -defined the carrier of y -valued Function-like non empty V24( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of y:]
x1 . x2 is Element of the carrier of y
x1 . u2 is Element of the carrier of y
wy is Relation-like the carrier of WY -defined the carrier of T1 -valued Function-like non empty V24( the carrier of WY) quasi_total Element of bool [: the carrier of WY, the carrier of T1:]
wy . u1 is Element of the carrier of T1
wy . y1 is Element of the carrier of T1
rng wy is Element of bool the carrier of T1
bool the carrier of T1 is non empty set
L is RelStr
the carrier of L is set
S is RelStr
the carrier of S is set
[: the carrier of L, the carrier of S:] is set
bool [: the carrier of L, the carrier of S:] is non empty set
S is RelStr
the carrier of S is set
[: 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 L, the carrier of S:] is set
bool [: the carrier of L, the carrier of S:] is non empty set
SS is Relation-like the carrier of L -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of S:]
Wy is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
Wy * SS is Relation-like the carrier of L -defined the carrier of S -valued Function-like Element of bool [: the carrier of L, the carrier of S:]
T is Relation-like the carrier of L -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of S:]
WY is non empty RelStr
the carrier of WY is non empty set
T1 is non empty RelStr
the carrier of T1 is non empty set
[: the carrier of WY, the carrier of T1:] is non empty set
bool [: the carrier of WY, the carrier of T1:] is non empty set
wy is non empty RelStr
the carrier of wy is non empty set
[: the carrier of T1, the carrier of wy:] is non empty set
bool [: the carrier of T1, the carrier of wy:] is non empty set
[: the carrier of T1, the carrier of WY:] is non empty set
bool [: the carrier of T1, the carrier of WY:] is non empty set
x is Relation-like the carrier of WY -defined the carrier of T1 -valued Function-like non empty V24( the carrier of WY) quasi_total Element of bool [: the carrier of WY, the carrier of T1:]

x1 is Relation-like the carrier of T1 -defined the carrier of WY -valued Function-like non empty V24( the carrier of T1) quasi_total Element of bool [: the carrier of T1, the carrier of WY:]
[: the carrier of wy, the carrier of T1:] is non empty set
bool [: the carrier of wy, the carrier of T1:] is non empty set
y is Relation-like the carrier of T1 -defined the carrier of wy -valued Function-like non empty V24( the carrier of T1) quasi_total Element of bool [: the carrier of T1, the carrier of wy:]

x2 is Relation-like the carrier of wy -defined the carrier of T1 -valued Function-like non empty V24( the carrier of wy) quasi_total Element of bool [: the carrier of wy, the carrier of T1:]
y * x is Relation-like the carrier of WY -defined the carrier of wy -valued Function-like non empty V24( the carrier of WY) quasi_total Element of bool [: the carrier of WY, the carrier of wy:]
[: the carrier of WY, the carrier of wy:] is non empty set
bool [: the carrier of WY, the carrier of wy:] is non empty set
x1 * x2 is Relation-like the carrier of wy -defined the carrier of WY -valued Function-like non empty V24( the carrier of wy) quasi_total Element of bool [: the carrier of wy, the carrier of WY:]
[: the carrier of wy, the carrier of WY:] is non empty set
bool [: the carrier of wy, the carrier of WY:] is non empty set
(y * x) " is Relation-like Function-like set

the carrier of L is set
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is strict TopSpace-like TopStruct

the carrier of S is set
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

the carrier of S is set
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

the carrier of SS is set
the topology of SS is non empty Element of bool (bool the carrier of SS)
bool the carrier of SS is non empty set
bool (bool the carrier of SS) is non empty set
TopStruct(# the carrier of SS, the topology of SS #) is strict TopSpace-like TopStruct

the carrier of [:S,SS:] is set
bool the carrier of [:S,SS:] is non empty set
bool (bool the carrier of [:S,SS:]) is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of S, b2 is Element of bool the carrier of SS : ( b1 in the topology of S & b2 in the topology of SS ) } is set
{ (union b1) where b1 is Element of bool (bool the carrier of [:S,SS:]) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of S, b3 is Element of bool the carrier of SS : ( b1 in the topology of S & b2 in the topology of SS ) } } is set
the carrier of [:L,S:] is set
[: the carrier of L, the carrier of S:] is set
the topology of [:L,S:] is non empty Element of bool (bool the carrier of [:L,S:])
bool the carrier of [:L,S:] is non empty set
bool (bool the carrier of [:L,S:]) is non empty set
the topology of [:S,SS:] is non empty Element of bool (bool the carrier of [:S,SS:])
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (ContMaps (L,S)) is functional non empty set
bool the carrier of (ContMaps (L,S)) is non empty set
S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty set
bool [: the carrier of L, the carrier of S:] is non empty set
S is functional non empty directed Element of bool the carrier of (ContMaps (L,S))
"\/" (S,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)
the carrier of (S |^ the carrier of L) is functional non empty set
Funcs ( the carrier of L, the carrier of S) is functional non empty FUNCTION_DOMAIN of the carrier of L, the carrier of S
bool the carrier of (S |^ the carrier of L) is non empty set
bool the carrier of S is non empty set
WY is Element of bool the carrier of S
T1 is set
Wy is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]
Wy " WY is Element of bool the carrier of L
bool the carrier of L is non empty set
Wy . T1 is set

product ( the carrier of L --> S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
wy is Element of the carrier of L
( the carrier of L --> S) . wy is non empty reflexive transitive antisymmetric non void RelStr
T is functional non empty directed Element of bool the carrier of (S |^ the carrier of L)
pi (T,wy) is non empty Element of bool the carrier of S
"\/" (T,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)
("\/" (T,(S |^ the carrier of L))) . wy is Element of the carrier of S
"\/" ((pi (T,wy)),S) is Element of the carrier of S
x is set

y . wy is set
x1 is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of S:]
x1 " WY is Element of bool the carrier of L

x2 is Element of bool the carrier of L
dom Wy is Element of bool the carrier of L
u2 is set
x1 . u2 is set
u1 is Element of the carrier of L
( the carrier of L --> S) . u1 is non empty reflexive transitive antisymmetric non void RelStr
pi (T,u1) is non empty Element of bool the carrier of S
Wy . u1 is Element of the carrier of S
"\/" ((pi (T,u1)),S) is Element of the carrier of S
x1 . u1 is Element of the carrier of S
dom x1 is Element of bool the carrier of L
wy is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric up-complete non void RelStr
S is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of S |^ the carrier of L
the carrier of S is functional non empty set
bool the carrier of S is non empty set
SS is functional directed Element of bool the carrier of S
"\/" (SS,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)
the carrier of (S |^ the carrier of L) is functional non empty set
Wy is functional non empty directed Element of bool the carrier of S
"\/" (Wy,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)
the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty set
bool [: the carrier of L, the carrier of S:] is non empty set
L is TopStruct
the carrier of L is set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is strict TopStruct
S is TopStruct
the carrier of S is set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopStruct
S is non empty TopRelStr
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 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
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) is strict TopRelStr
SS is non empty TopRelStr
the carrier of SS is non empty set
the InternalRel of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Element of bool [: the carrier of SS, the carrier of SS:]
[: the carrier of SS, the carrier of SS:] is non empty set
bool [: the carrier of SS, the carrier of SS:] is non empty set
the topology of SS is Element of bool (bool the carrier of SS)
bool the carrier of SS is non empty set
bool (bool the carrier of SS) is non empty set
TopRelStr(# the carrier of SS, the InternalRel of SS, the topology of SS #) is strict TopRelStr
ContMaps (L,S) is strict RelStr
ContMaps (S,SS) is strict RelStr
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
RelStr(# the carrier of SS, the InternalRel of SS #) is strict RelStr
S |^ the carrier of L is non empty V185() strict RelStr
SS |^ the carrier of S is non empty V185() strict RelStr
the carrier of (ContMaps (L,S)) is set
the carrier of (ContMaps (S,SS)) is set
WY is set
[: the carrier of L, the carrier of S:] is set
bool [: the carrier of L, the carrier of S:] is non empty set
T1 is Relation-like the carrier of L -defined the carrier of S -valued Function-like V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]
[: the carrier of S, the carrier of SS:] is set
bool [: the carrier of S, the carrier of SS:] is non empty set
wy is Relation-like the carrier of S -defined the carrier of SS -valued Function-like V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of SS:]
x is Element of bool the carrier of SS
wy " x is Element of bool the carrier of S
[#] SS is non empty non proper dense lower upper Element of bool the carrier of SS
([#] SS) \ x is Element of bool the carrier of SS
[#] S is non empty non proper dense lower upper Element of bool the carrier of S
y is Element of bool the carrier of S
([#] S) \ y is Element of bool the carrier of S
T1 " y is Element of bool the carrier of L
[#] L is non proper dense Element of bool the carrier of L
([#] L) \ (T1 " y) is Element of bool the carrier of L
([#] L) \ (wy " x) is Element of bool the carrier of L
[#] S is non proper dense Element of bool the carrier of S
([#] S) \ (wy " x) is Element of bool the carrier of S
WY is set
[: the carrier of S, the carrier of SS:] is set
bool [: the carrier of S, the carrier of SS:] is non empty set
T1 is Relation-like the carrier of S -defined the carrier of SS -valued Function-like V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of SS:]
[: the carrier of L, the carrier of S:] is set
bool [: the carrier of L, the carrier of S:] is non empty set
wy is Relation-like the carrier of L -defined the carrier of S -valued Function-like V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]
x is Element of bool the carrier of S
wy " x is Element of bool the carrier of L
[#] S is non empty non proper dense lower upper Element of bool the carrier of S
([#] S) \ x is Element of bool the carrier of S
y is Element of bool the carrier of SS
([#] S) \ y is Element of bool the carrier of S
[#] SS is non empty non proper dense lower upper Element of bool the carrier of SS
([#] SS) \ y is Element of bool the carrier of SS
T1 " y is Element of bool the carrier of S
[#] S is non proper dense Element of bool the carrier of S
([#] S) \ (T1 " y) is Element of bool the carrier of S
([#] S) \ (wy " x) is Element of bool the carrier of S
[#] L is non proper dense Element of bool the carrier of L
([#] L) \ (wy " x) is Element of bool the carrier of L
T is full SubRelStr of S |^ the carrier of L
the carrier of T is set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
Wy is full SubRelStr of S |^ the carrier of L
the carrier of Wy is set
the InternalRel of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Element of bool [: the carrier of Wy, the carrier of Wy:]
[: the carrier of Wy, the carrier of Wy:] is set
bool [: the carrier of Wy, the carrier of Wy:] is non empty set
RelStr(# the carrier of Wy, the InternalRel of Wy #) is strict RelStr

L is non empty TopSpace-like TopStruct

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of L is non empty set
S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric up-complete non void RelStr
L is non empty set

the carrier of () is functional non empty set
bool the carrier of () is non empty set
Wy is Element of L
S . Wy is non empty reflexive transitive antisymmetric non void RelStr
S . Wy is non empty reflexive non void RelStr
SS is functional non empty directed Element of bool the carrier of ()
pi (SS,Wy) is non empty Element of bool the carrier of (S . Wy)
the carrier of (S . Wy) is non empty set
bool the carrier of (S . Wy) is non empty set
L is non empty set
bool L is non empty set

the carrier of () is functional non empty set
Wy is Relation-like Function-like Element of the carrier of ()
T is Relation-like Function-like Element of the carrier of ()
WY is Element of L
S . WY is non empty reflexive non void RelStr
Wy . WY is Element of the carrier of (S . WY)
the carrier of (S . WY) is non empty set
T . WY is Element of the carrier of (S . WY)
S . WY is non empty reflexive transitive antisymmetric non void RelStr
the carrier of (S . WY) is non empty set
bool the carrier of (S . WY) is non empty set
T1 is non empty directed Element of bool the carrier of (S . WY)
"\/" (T1,(S . WY)) is Element of the carrier of (S . WY)
"\/" (T1,(S . WY)) is Element of the carrier of (S . WY)
the Element of T1 is Element of T1
{ (T +* (WY,b1)) where b1 is Element of the carrier of (S . WY) : b1 in T1 } is set
proj1 T is set
x1 is set
x2 is Element of the carrier of (S . WY)
T +* (WY,x2) is Relation-like Function-like set
u2 is Element of L
(T +* (WY,x2)) . u2 is set
T . u2 is Element of the carrier of (S . u2)
S . u2 is non empty reflexive non void RelStr
the carrier of (S . u2) is non empty set
S . u2 is non empty reflexive transitive antisymmetric non void RelStr
the carrier of (S . u2) is non empty set
proj1 (T +* (WY,x2)) is set
bool the carrier of () is non empty set
y is Element of the carrier of (S . WY)
T +* (WY,y) is Relation-like Function-like set
x1 is functional Element of bool the carrier of ()
x2 is functional non empty Element of bool the carrier of ()
u2 is Relation-like Function-like Element of the carrier of ()
u1 is Relation-like Function-like Element of the carrier of ()
y1 is Element of the carrier of (S . WY)
T +* (WY,y1) is Relation-like Function-like set
y2 is Element of the carrier of (S . WY)
T +* (WY,y2) is Relation-like Function-like set
y1 is Element of the carrier of (S . WY)
T +* (WY,y1) is Relation-like Function-like set
y2 is Relation-like Function-like Element of the carrier of ()
v2 is Element of L
y2 . v2 is Element of the carrier of (S . v2)
S . v2 is non empty reflexive non void RelStr
the carrier of (S . v2) is non empty set
u2 . v2 is Element of the carrier of (S . v2)
T . v2 is Element of the carrier of (S . v2)
v2 is Element of L
y2 . v2 is Element of the carrier of (S . v2)
S . v2 is non empty reflexive non void RelStr
the carrier of (S . v2) is non empty set
u1 . v2 is Element of the carrier of (S . v2)
T . v2 is Element of the carrier of (S . v2)
u2 is functional non empty directed Element of bool the carrier of ()
pi (u2,WY) is non empty Element of bool the carrier of (S . WY)
bool the carrier of (S . WY) is non empty set
u1 is set
y1 is Element of the carrier of (S . WY)
T +* (WY,y1) is Relation-like Function-like set
(T +* (WY,y1)) . WY is set
u1 is Element of L
S . u1 is non empty reflexive transitive antisymmetric non void RelStr
"\/" ((pi (u2,WY)),(S . WY)) is Element of the carrier of (S . WY)

"\/" (u2,()) is Relation-like Function-like Element of the carrier of ()
("\/" (u2,())) . u1 is Element of the carrier of (S . u1)
S . u1 is non empty reflexive non void RelStr
the carrier of (S . u1) is non empty set
pi (u2,u1) is non empty Element of bool the carrier of (S . u1)
bool the carrier of (S . u1) is non empty set
"\/" ((pi (u2,u1)),(S . u1)) is Element of the carrier of (S . u1)
(T +* (WY,y)) . u1 is set
T . u1 is Element of the carrier of (S . u1)
u1 is Relation-like Function-like Element of the carrier of ()
y1 is Element of the carrier of (S . WY)
T +* (WY,y1) is Relation-like Function-like set
u1 . WY is Element of the carrier of (S . WY)
{ b1 where b1 is Element of L : not Wy . b1 = Bottom (S . b1) } is set
T1 is set
wy is Element of L
Wy . wy is Element of the carrier of (S . wy)
S . wy is non empty reflexive non void RelStr
the carrier of (S . wy) is non empty set
S . wy is non empty reflexive transitive antisymmetric non void RelStr
Bottom (S . wy) is Element of the carrier of (S . wy)
the carrier of (S . wy) is non empty set
"\/" ({},(S . wy)) is Element of the carrier of (S . wy)

x is Element of L
wy . x is set
S . x is non empty reflexive transitive antisymmetric non void RelStr
Bottom (S . x) is Element of the carrier of (S . x)
the carrier of (S . x) is non empty set
"\/" ({},(S . x)) is Element of the carrier of (S . x)
dom wy is Element of bool L
x is Relation-like Function-like Element of the carrier of ()
{ (x +* (T | b1)) where b1 is finite Element of bool L : verum } is set
x1 is set
x2 is finite Element of bool L

x +* (T | x2) is Relation-like Function-like set
proj1 T is set
proj1 (T | x2) is finite set
u2 is Element of L
(x +* (T | x2)) . u2 is set
x . u2 is Element of the carrier of (S . u2)
S . u2 is non empty reflexive non void RelStr
the carrier of (S . u2) is non empty set
(T | x2) . u2 is set
T . u2 is Element of the carrier of (S . u2)
S . u2 is non empty reflexive transitive antisymmetric non void RelStr
the carrier of (S . u2) is non empty set
L \/ (proj1 (T | x2)) is set
proj1 (x +* (T | x2)) is set
bool the carrier of () is non empty set

x +* (T | ({} L)) is Relation-like Function-like set
x1 is functional Element of bool the carrier of ()
x2 is functional non empty Element of bool the carrier of ()
u2 is Relation-like Function-like Element of the carrier of ()
u1 is Relation-like Function-like Element of the carrier of ()
y1 is finite Element of bool L

x +* (T | y1) is Relation-like Function-like set
y2 is finite Element of bool L

x +* (T | y2) is Relation-like Function-like set
y1 \/ y2 is finite Element of bool L
y1 is finite Element of bool L

x +* (T | y1) is Relation-like Function-like set
y2 is Relation-like Function-like Element of the carrier of ()
proj1 T is set
proj1 (T | y1) is finite set
proj1 (T | y1) is finite set
v2 is Element of L
x . v2 is Element of the carrier of (S . v2)
S . v2 is non empty reflexive non void RelStr
the carrier of (S . v2) is non empty set
S . v2 is non empty reflexive transitive antisymmetric non void RelStr
Bottom (S . v2) is Element of the carrier of (S . v2)
the carrier of (S . v2) is non empty set
"\/" ({},(S . v2)) is Element of the carrier of (S . v2)
T . v2 is Element of the carrier of (S . v2)
y2 . v2 is Element of the carrier of (S . v2)
(T | y1) . v2 is set
u2 . v2 is Element of the carrier of (S . v2)
y2 . v2 is Element of the carrier of (S . v2)
u2 . v2 is Element of the carrier of (S . v2)
y2 . v2 is Element of the carrier of (S . v2)
(T | y1) . v2 is set
u2 . v2 is Element of the carrier of (S . v2)
(T | y1) . v2 is set
proj1 (T | y2) is finite set
v2 is Element of L
x . v2 is Element of the carrier of (S . v2)
S . v2 is non empty reflexive non void RelStr
the carrier of (S . v2) is non empty set
S . v2 is non empty reflexive transitive antisymmetric non void RelStr
Bottom (S . v2) is Element of the carrier of (S . v2)
the carrier of (S . v2) is non empty set
"\/" ({},(S . v2)) is Element of the carrier of (S . v2)
T . v2 is Element of the carrier of (S . v2)
y2 . v2 is Element of the carrier of (S . v2)
(T | y1) . v2 is set
u1 . v2 is Element of the carrier of (S . v2)
y2 . v2 is Element of the carrier of (S . v2)
u1 . v2 is Element of the carrier of (S . v2)
y2 . v2 is Element of the carrier of (S . v2)
(T | y1) . v2 is set
u1 . v2 is Element of the carrier of (S . v2)
(T | y2) . v2 is set
u1 is Element of L

y1 is finite Element of bool L

x +* (T | y1) is Relation-like Function-like set
u2 is functional non empty directed Element of bool the carrier of ()

"\/" (u2,()) is Relation-like Function-like Element of the carrier of ()
y2 is Relation-like Function-like Element of the carrier of ()
proj1 T is set
proj1 (T | y1) is finite set
(T | y1) . u1 is set
T . u1 is Element of the carrier of (S . u1)
S . u1 is non empty reflexive non void RelStr
the carrier of (S . u1) is non empty set
y2 . u1 is Element of the carrier of (S . u1)
("\/" (u2,())) . u1 is Element of the carrier of (S . u1)
u1 is Relation-like Function-like Element of the carrier of ()
y1 is finite Element of bool L

x +* (T | y1) is Relation-like Function-like set
T1 is Element of bool L
proj1 (T | y1) is finite set
y2 is set
y1 is Element of L
Wy . y1 is Element of the carrier of (S . y1)
S . y1 is non empty reflexive non void RelStr
the carrier of (S . y1) is non empty set
S . y1 is non empty reflexive transitive antisymmetric non void RelStr
Bottom (S . y1) is Element of the carrier of (S . y1)
the carrier of (S . y1) is non empty set
"\/" ({},(S . y1)) is Element of the carrier of (S . y1)
u1 . y1 is Element of the carrier of (S . y1)
x . y1 is Element of the carrier of (S . y1)
y2 is finite Element of bool L
y1 is finite Element of bool L
y2 is Element of L
Wy . y2 is Element of the carrier of (S . y2)
S . y2 is non empty reflexive non void RelStr
the carrier of (S . y2) is non empty set
S . y2 is non empty reflexive transitive antisymmetric non void RelStr
Bottom (S . y2) is Element of the carrier of (S . y2)
the carrier of (S . y2) is non empty set
"\/" ({},(S . y2)) is Element of the carrier of (S . y2)
WY is finite Element of bool L
T1 is functional non empty directed Element of bool the carrier of ()
"\/" (T1,()) is Relation-like Function-like Element of the carrier of ()
wy is set
x is Element of L
S . x is non empty reflexive non void RelStr
pi (T1,x) is non empty Element of bool the carrier of (S . x)
the carrier of (S . x) is non empty set
bool the carrier of (S . x) is non empty set
S . x is non empty reflexive transitive antisymmetric non void RelStr
the carrier of (S . x) is non empty set
y is Element of the carrier of (S . x)
x1 is Element of the carrier of (S . x)

x2 . x is set

u2 . x is set
u1 is Relation-like Function-like Element of the carrier of ()
y1 is Relation-like Function-like Element of the carrier of ()
y2 is Relation-like Function-like Element of the carrier of ()
y2 . x is Element of the carrier of (S . x)
("\/" (T1,())) . x is Element of the carrier of (S . x)
"\/" ((pi (T1,x)),(S . x)) is Element of the carrier of (S . x)
Wy . x is Element of the carrier of (S . x)
T . x is Element of the carrier of (S . x)
S . x is non empty reflexive transitive antisymmetric non void RelStr
the carrier of (S . x) is non empty set
y is Element of the carrier of (S . x)

x1 . x is set
x2 is set
u2 is set

proj1 wy is set
proj2 wy is set
bool T1 is non empty set
x is functional finite Element of bool T1
y is Relation-like Function-like Element of the carrier of ()
x1 is Element of L
S . x1 is non empty reflexive transitive antisymmetric non void RelStr
wy . x1 is set
x2 is Element of L
u2 is Relation-like Function-like Element of the carrier of ()
S . x2 is non empty reflexive non void RelStr
Wy . x2 is Element of the carrier of (S . x2)
the carrier of (S . x2) is non empty set
u2 . x2 is Element of the carrier of (S . x2)
S . x1 is non empty reflexive non void RelStr
u2 . x1 is Element of the carrier of (S . x1)
the carrier of (S . x1) is non empty set
y . x1 is Element of the carrier of (S . x1)
Wy . x1 is Element of the carrier of (S . x1)
Wy . x1 is Element of the carrier of (S . x1)
S . x1 is non empty reflexive non void RelStr
the carrier of (S . x1) is non empty set
Bottom (S . x1) is Element of the carrier of (S . x1)
the carrier of (S . x1) is non empty set
"\/" ({},(S . x1)) is Element of the carrier of (S . x1)
y . x1 is Element of the carrier of (S . x1)
L is set

S |^ L is non empty V185() strict reflexive antisymmetric non void RelStr
the carrier of S is non empty set
Bottom S is Element of the carrier of S
"\/" ({},S) is Element of the carrier of S
L --> () is Relation-like L -defined the carrier of S -valued Function-like constant V24(L) quasi_total Element of bool [:L, the carrier of S:]
[:L, the carrier of S:] is set
bool [:L, the carrier of S:] is non empty set
rng (L --> ()) is trivial finite Element of bool the carrier of S
bool the carrier of S is non empty set
the carrier of (S |^ L) is functional non empty set
Funcs (L, the carrier of S) is functional non empty FUNCTION_DOMAIN of L, the carrier of S
dom (L --> ()) is Element of bool L
bool L is non empty set
S is Relation-like Function-like Element of the carrier of (S |^ L)
SS is Relation-like Function-like Element of the carrier of (S |^ L)
Wy is non empty set
S |^ Wy is non empty V185() strict reflexive antisymmetric non void RelStr
the carrier of (S |^ Wy) is functional non empty set
T is Relation-like Function-like Element of the carrier of (S |^ Wy)
T1 is Element of Wy
T . T1 is Element of the carrier of S
WY is Relation-like Function-like Element of the carrier of (S |^ Wy)
WY . T1 is Element of the carrier of S
L is non empty TopSpace-like TopStruct

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (ContMaps (L,S)) is functional non empty set
Bottom S is Element of the carrier of S
the carrier of S is non empty set
"\/" ({},S) is Element of the carrier of S
L --> () is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of S:]
the carrier of L is non empty set
[: the carrier of L, the carrier of S:] is non empty set
bool [: the carrier of L, the carrier of S:] is non empty set
the carrier of L --> () is Relation-like the carrier of L -defined the carrier of S -valued Function-like constant non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]
S is Relation-like Function-like Element of the carrier of (ContMaps (L,S))
SS is Relation-like Function-like Element of the carrier of (ContMaps (L,S))
S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric lower-bounded non void RelStr
the carrier of (S |^ the carrier of L) is functional non empty set

the carrier of () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
() --> () is Relation-like the carrier of () -defined the carrier of S -valued Function-like non empty V24( the carrier of ()) quasi_total continuous monotone Element of bool [: the carrier of (), the carrier of S:]
[: the carrier of (), the carrier of S:] is non empty set
bool [: the carrier of (), the carrier of S:] is non empty set
the carrier of () --> () is Relation-like the carrier of () -defined the carrier of S -valued Function-like constant non empty V24( the carrier of ()) quasi_total quasi_total monotone Element of bool [: the carrier of (), the carrier of S:]
Bottom (S |^ the carrier of L) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)
"\/" ({},(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)
Wy is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

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

the carrier of S is non empty set
bool the carrier of S is non empty set
the topology of S is Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
S is Element of bool (bool the carrier of S)
union S is Element of bool the carrier of S
SS is non empty directed Element of bool the carrier of S
"\/" (SS,S) is Element of the carrier of S
Wy is set
T is Element of bool the carrier of S
WY is set
SS is Element of bool the carrier of S
S is Element of bool the carrier of S
SS is Element of bool the carrier of S
S /\ SS is Element of bool the carrier of S
T is Element of bool the carrier of S
Wy is Element of bool the carrier of S
WY is non empty directed Element of bool the carrier of S
"\/" (WY,S) is Element of the carrier of S
T1 is set
wy is set
x is Element of the carrier of S
y is Element of the carrier of S
x1 is Element of the carrier of S

the carrier of L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 is Element of bool the carrier of L : ( b1 is upper & b1 is inaccessible_by_directed_joins ) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
S is set
SS is Element of bool the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
S is Element of bool (bool the carrier of L)
TopRelStr(# the carrier of L, the InternalRel of L,S #) is strict TopRelStr
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #) is set
the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,S #) is Relation-like the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #) -defined the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #):]
[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #):] is set
bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #):] is non empty set
RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,S #) #) is strict RelStr

the carrier of Wy is non empty set
bool the carrier of Wy is non empty set
T is Element of bool the carrier of Wy
WY is Element of bool the carrier of L
WY is Element of bool the carrier of L
the topology of Wy is Element of bool (bool the carrier of Wy)
bool (bool the carrier of Wy) is non empty set

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 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 InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty 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, the InternalRel of S #) is strict RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty 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, the InternalRel of S #) is strict RelStr
SS is set

T is Element of bool the carrier of S
SS is set

T is Element of bool the carrier of S

the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is strict TopRelStr

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 non empty 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
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) is strict TopRelStr
S is Element of bool the carrier of S
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
SS is Element of bool the carrier of L
SS is Element of bool the carrier of L

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 non empty 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, the InternalRel of S #) is strict RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict 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 non empty 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, the InternalRel of S #) is strict RelStr

the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is strict TopRelStr
the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is set
the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is Relation-like the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) -defined the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #):]
[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #):] is set
bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #):] is non empty set
RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) #) is strict RelStr
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict 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 non empty 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, the InternalRel of S #) is strict 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 non empty 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), the InternalRel of (S) #) is strict RelStr
the carrier of (L) is non empty set
the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty set
bool [: the carrier of (L), the carrier of (L):] is non empty set
RelStr(# the carrier of (L), the InternalRel of (L) #) is strict RelStr

the carrier of L is non empty set

the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty set
bool [: the carrier of L, the carrier of S:] is non empty set
S is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]

the carrier of (L) is non empty set

the carrier of (S) is non empty set
[: the carrier of (L), the carrier of (S):] is non empty set
bool [: the carrier of (L), the carrier of (S):] is non empty set
the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty set
bool [: the carrier of (L), the carrier of (L):] is non empty set
RelStr(# the carrier of (L), the InternalRel of (L) #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty 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), the InternalRel of (S) #) is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty 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, the InternalRel of S #) is strict RelStr

the carrier of L is non empty set

the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty set
bool [: the carrier of L, the carrier of S:] is non empty set

S is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total directed-sups-preserving Element of bool [: the carrier of L, the carrier of S:]
(L,S,S) is Relation-like the carrier of (L) -defined the carrier of (S) -valued Function-like non empty V24( the carrier of (L)) quasi_total Element of bool [: the carrier of (L), the carrier of (S):]
the carrier of (L) is non empty set
the carrier of (S) is non empty set
[: the carrier of (L), the carrier of (S):] is non empty set
bool [: the carrier of (L), the carrier of (S):] is non empty set
the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty set
bool [: the carrier of (L), the carrier of (L):] is non empty set
RelStr(# the carrier of (L), the InternalRel of (L) #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty 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), the InternalRel of (S) #) is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty 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, the InternalRel of S #) is strict RelStr

the carrier of L is non empty set

the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty set
bool [: the carrier of L, the carrier of S:] is non empty set

S is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]
(L,S,S) is Relation-like the carrier of (L) -defined the carrier of (S) -valued Function-like non empty V24( the carrier of (L)) quasi_total Element of bool [: the carrier of (L), the carrier of (S):]
the carrier of (L) is non empty set
the carrier of (S) is non empty set
[: the carrier of (L), the carrier of (S):] is non empty set
bool [: the carrier of (L), the carrier of (S):] is non empty set
the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty set
bool [: the carrier of (L), the carrier of (L):] is non empty set
RelStr(# the carrier of (L), the InternalRel of (L) #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty 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), the InternalRel of (S) #) is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty 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, the InternalRel of S #) is strict RelStr
L is non empty TopSpace-like TopStruct

oContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr