:: WAYBEL_9 semantic presentation

K156() is set
K160() is non empty V39() V40() V41() non finite cardinal limit_cardinal Element of K10(K156())
K10(K156()) is non empty cup-closed diff-closed preBoolean set
K133() is non empty V39() V40() V41() non finite cardinal limit_cardinal set
K10(K133()) is non empty cup-closed diff-closed preBoolean non finite set
1 is non empty V39() V40() V41() V45() finite cardinal Element of K160()
K11(1,1) is non empty set
K10(K11(1,1)) is non empty cup-closed diff-closed preBoolean set
K11(K11(1,1),1) is non empty set
K10(K11(K11(1,1),1)) is non empty cup-closed diff-closed preBoolean set
K11(K11(1,1),K156()) is set
K10(K11(K11(1,1),K156())) is non empty cup-closed diff-closed preBoolean set
K11(K156(),K156()) is set
K11(K11(K156(),K156()),K156()) is set
K10(K11(K11(K156(),K156()),K156())) is non empty cup-closed diff-closed preBoolean set
2 is non empty V39() V40() V41() V45() finite cardinal Element of K160()
K11(2,2) is non empty set
K11(K11(2,2),K156()) is set
K10(K11(K11(2,2),K156())) is non empty cup-closed diff-closed preBoolean set
{} is empty Function-like functional V39() V40() V41() V43() V44() V45() finite cardinal {} -element set
the empty Function-like functional V39() V40() V41() V43() V44() V45() finite cardinal {} -element set is empty Function-like functional V39() V40() V41() V43() V44() V45() finite cardinal {} -element set
{{},1} is non empty set
K10(K160()) is non empty cup-closed diff-closed preBoolean non finite set
S is non empty RelStr
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
the carrier of S is non empty set
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
S is non empty RelStr
the carrier of S is non empty set
x is non empty RelStr
the carrier of x is non empty set
K11( the carrier of S, the carrier of x) is non empty set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is non empty Relation-like the carrier of S -defined the carrier of x -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
d is Element of the carrier of S
X is Element of the carrier of S
c₃ . X is Element of the carrier of x
c₃ . d is Element of the carrier of x
d is Element of the carrier of S
X is Element of the carrier of S
xM is Element of the carrier of x
c₃ . d is Element of the carrier of x
x is Element of the carrier of x
c₃ . X is Element of the carrier of x
S is RelStr
the carrier of S is set
x is RelStr
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
c₃ is non empty RelStr
the carrier of c₃ is non empty set
d is non empty RelStr
the carrier of d is non empty set
K11( the carrier of c₃, the carrier of d) is non empty set
K10(K11( the carrier of c₃, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is non empty set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is non empty set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
X is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
xM is non empty Relation-like the carrier of c₃ -defined the carrier of d -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of d) Element of K10(K11( the carrier of c₃, the carrier of d))
A is Element of the carrier of c₃
M is Element of the carrier of c₃
xM . A is Element of the carrier of d
xM . M is Element of the carrier of d
x is non empty RelStr
the carrier of x is non empty set
x is non empty RelStr
the carrier of x is non empty set
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
R is Element of the carrier of x
i2 is Element of the carrier of x
j2 is non empty Relation-like the carrier of x -defined the carrier of x -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of x) Element of K10(K11( the carrier of x, the carrier of x))
j2 . R is Element of the carrier of x
j2 . i2 is Element of the carrier of x
xM . A is Element of the carrier of d
xM . M is Element of the carrier of d
S is RelStr
the carrier of S is set
x is RelStr
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
c₃ is non empty RelStr
the carrier of c₃ is non empty set
d is non empty RelStr
the carrier of d is non empty set
K11( the carrier of c₃, the carrier of d) is non empty set
K10(K11( the carrier of c₃, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is non empty set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is non empty set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
X is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
xM is non empty Relation-like the carrier of c₃ -defined the carrier of d -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of d) Element of K10(K11( the carrier of c₃, the carrier of d))
A is Element of the carrier of c₃
M is Element of the carrier of c₃
xM . M is Element of the carrier of d
xM . A is Element of the carrier of d
x is non empty RelStr
the carrier of x is non empty set
x is non empty RelStr
the carrier of x is non empty set
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
R is Element of the carrier of x
i2 is Element of the carrier of x
j2 is non empty Relation-like the carrier of x -defined the carrier of x -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of x) Element of K10(K11( the carrier of x, the carrier of x))
j2 . i2 is Element of the carrier of x
j2 . R is Element of the carrier of x
S is 1-sorted
the carrier of S is set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is 1-sorted
the carrier of x is set
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of K10(K10( the carrier of S))
d is Element of K10(K10( the carrier of x))
S is non empty reflexive antisymmetric with_infima RelStr
the carrier of S is non empty set
x is Element of the carrier of S
uparrow x is non empty filtered Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
uparrow {x} is non empty Element of K10( the carrier of S)
{ b₁ where b₁ is Element of the carrier of S : b₁ "/\" x = x } is set
c₃ is set
d is Element of the carrier of S
d "/\" x is Element of the carrier of S
c₃ is set
d is Element of the carrier of S
d "/\" x is Element of the carrier of S
S is non empty reflexive antisymmetric with_suprema RelStr
the carrier of S is non empty set
[#] S is non empty non proper directed lower upper Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of S
uparrow x is non empty filtered Element of K10( the carrier of S)
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
uparrow {x} is non empty Element of K10( the carrier of S)
{x} "\/" ([#] S) is non empty Element of K10( the carrier of S)
{ (x "\/" b₁) where b₁ is Element of the carrier of S : b₁ in [#] S } is set
c₃ is set
d is Element of the carrier of S
x "\/" d is Element of the carrier of S
c₃ is set
d is Element of the carrier of S
x "\/" d is Element of the carrier of S
S is non empty reflexive antisymmetric with_suprema RelStr
the carrier of S is non empty set
x is Element of the carrier of S
downarrow x is non empty directed Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
downarrow {x} is non empty Element of K10( the carrier of S)
{ b₁ where b₁ is Element of the carrier of S : b₁ "\/" x = x } is set
c₃ is set
d is Element of the carrier of S
d "\/" x is Element of the carrier of S
c₃ is set
d is Element of the carrier of S
d "\/" x is Element of the carrier of S
S is non empty reflexive antisymmetric with_infima RelStr
the carrier of S is non empty set
[#] S is non empty non proper filtered lower upper Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of S
downarrow x is non empty directed Element of K10( the carrier of S)
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
downarrow {x} is non empty Element of K10( the carrier of S)
{x} "/\" ([#] S) is non empty Element of K10( the carrier of S)
{ (x "/\" b₁) where b₁ is Element of the carrier of S : b₁ in [#] S } is set
c₃ is set
d is Element of the carrier of S
x "/\" d is Element of the carrier of S
c₃ is set
d is Element of the carrier of S
x "/\" d is Element of the carrier of S
S is non empty reflexive antisymmetric with_infima RelStr
the carrier of S is non empty set
x is Element of the carrier of S
x "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
uparrow x is non empty filtered Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
uparrow {x} is non empty Element of K10( the carrier of S)
(x "/\") .: (uparrow x) is non empty Element of K10( the carrier of S)
c₃ is set
dom (x "/\") is Element of K10( the carrier of S)
d is set
(x "/\") . d is set
X is Element of the carrier of S
x "/\" X is Element of the carrier of S
c₃ is set
dom (x "/\") is Element of K10( the carrier of S)
x "/\" x is Element of the carrier of S
(x "/\") . x is Element of the carrier of S
S is non empty reflexive antisymmetric with_infima RelStr
the carrier of S is non empty set
x is Element of the carrier of S
x "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
(x "/\") " {x} is Element of K10( the carrier of S)
uparrow x is non empty filtered Element of K10( the carrier of S)
uparrow {x} is non empty Element of K10( the carrier of S)
c₃ is set
d is Element of the carrier of S
(x "/\") . d is Element of the carrier of S
x "/\" d is Element of the carrier of S
c₃ is set
d is Element of the carrier of S
(x "/\") . d is Element of the carrier of S
x "/\" d is Element of the carrier of S
dom (x "/\") is Element of K10( the carrier of S)
S is non empty 1-sorted
the carrier of S is non empty set
x is non empty NetStr over S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of x is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
the Element of the carrier of x is Element of the carrier of x
d is Element of the carrier of x
x . d is Element of the carrier of S
the mapping of x . d is Element of the carrier of S
S is non empty reflexive transitive RelStr
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is non empty directed Element of K10( the carrier of S)
K11(x, the carrier of S) is non empty set
K10(K11(x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S |_2 x is Relation-like x -defined x -valued Element of K10(K11(x,x))
K11(x,x) is non empty set
K10(K11(x,x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S /\ K11(x,x) is set
c₃ is non empty Relation-like x -defined the carrier of S -valued Function-like V34(x) V36(x, the carrier of S) Element of K10(K11(x, the carrier of S))
NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty strict NetStr over S
the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty set
the InternalRel of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is Relation-like the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) -defined the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) -valued Element of K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #)))
K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #)) is non empty set
K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #))) is non empty cup-closed diff-closed preBoolean set
X is SubRelStr of S
xM is reflexive transitive full SubRelStr of S
the carrier of xM is set
x is Element of the carrier of xM
[#] xM is non proper Element of K10( the carrier of xM)
K10( the carrier of xM) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of xM
A is Element of x
M is Element of x
R is Element of the carrier of S
i2 is Element of the carrier of xM
x is non empty directed NetStr over S
S is non empty reflexive RelStr
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is non empty directed Element of K10( the carrier of S)
K11(x, the carrier of S) is non empty set
K10(K11(x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S |_2 x is Relation-like x -defined x -valued Element of K10(K11(x,x))
K11(x,x) is non empty set
K10(K11(x,x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S /\ K11(x,x) is set
c₃ is non empty Relation-like x -defined the carrier of S -valued Function-like V34(x) V36(x, the carrier of S) Element of K10(K11(x, the carrier of S))
NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty strict NetStr over S
S is non empty reflexive transitive RelStr
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is non empty directed Element of K10( the carrier of S)
K11(x, the carrier of S) is non empty set
K10(K11(x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S |_2 x is Relation-like x -defined x -valued Element of K10(K11(x,x))
K11(x,x) is non empty set
K10(K11(x,x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S /\ K11(x,x) is set
c₃ is non empty Relation-like x -defined the carrier of S -valued Function-like V34(x) V36(x, the carrier of S) Element of K10(K11(x, the carrier of S))
NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty strict directed NetStr over S
S is non empty reflexive transitive RelStr
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of S
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
c₃ is non empty directed Element of K10( the carrier of S)
"\/" (c₃,S) is Element of the carrier of S
x "/\" ("\/" (c₃,S)) is Element of the carrier of S
{x} "/\" c₃ is non empty Element of K10( the carrier of S)
"\/" (({x} "/\" c₃),S) is Element of the carrier of S
K11(c₃, the carrier of S) is non empty set
K10(K11(c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id c₃ is non empty Relation-like c₃ -defined c₃ -valued Function-like one-to-one V34(c₃) V36(c₃,c₃) Element of K10(K11(c₃,c₃))
K11(c₃,c₃) is non empty set
K10(K11(c₃,c₃)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S |_2 c₃ is Relation-like c₃ -defined c₃ -valued Element of K10(K11(c₃,c₃))
the InternalRel of S /\ K11(c₃,c₃) is set
d is non empty Relation-like c₃ -defined the carrier of S -valued Function-like V34(c₃) V36(c₃, the carrier of S) Element of K10(K11(c₃, the carrier of S))
NetStr(# c₃,( the InternalRel of S |_2 c₃),d #) is non empty transitive strict directed NetStr over S
netmap (NetStr(# c₃,( the InternalRel of S |_2 c₃),d #),S) is non empty Relation-like the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #) -defined the carrier of S -valued Function-like V34( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #)) V36( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #), the carrier of S) Element of K10(K11( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #), the carrier of S))
the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #) is non empty set
K11( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #), the carrier of S) is non empty set
K10(K11( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #) is non empty Relation-like the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #) -defined the carrier of S -valued Function-like V34( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #)) V36( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #), the carrier of S) Element of K10(K11( the carrier of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #), the carrier of S))
\\/ ((netmap (NetStr(# c₃,( the InternalRel of S |_2 c₃),d #),S)),S) is Element of the carrier of S
sup NetStr(# c₃,( the InternalRel of S |_2 c₃),d #) is Element of the carrier of S
\\/ ( the mapping of NetStr(# c₃,( the InternalRel of S |_2 c₃),d #),S) is Element of the carrier of S
d .: c₃ is Element of K10( the carrier of S)
rng (netmap (NetStr(# c₃,( the InternalRel of S |_2 c₃),d #),S)) is Element of K10( the carrier of S)
x "/\" (\\/ ((netmap (NetStr(# c₃,( the InternalRel of S |_2 c₃),d #),S)),S)) is Element of the carrier of S
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty transitive directed NetStr over S
x "/\" c₃ is non empty strict directed NetStr over S
the carrier of (x "/\" c₃) is non empty set
X is Element of the carrier of (x "/\" c₃)
xM is Element of the carrier of (x "/\" c₃)
x is Element of the carrier of (x "/\" c₃)
the carrier of c₃ is non empty set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is non empty set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the InternalRel of (x "/\" c₃) is Relation-like the carrier of (x "/\" c₃) -defined the carrier of (x "/\" c₃) -valued Element of K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)))
K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)) is non empty set
K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c₃), the InternalRel of (x "/\" c₃) #) is strict RelStr
x is Element of the carrier of c₃
A is Element of the carrier of c₃
M is Element of the carrier of c₃
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty transitive directed NetStr over S
x "/\" c₃ is non empty strict directed NetStr over S
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty reflexive NetStr over S
x "/\" c₃ is non empty strict NetStr over S
the carrier of c₃ is non empty set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is non empty set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the carrier of (x "/\" c₃) is non empty set
the InternalRel of (x "/\" c₃) is Relation-like the carrier of (x "/\" c₃) -defined the carrier of (x "/\" c₃) -valued Element of K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)))
K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)) is non empty set
K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c₃), the InternalRel of (x "/\" c₃) #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty antisymmetric NetStr over S
x "/\" c₃ is non empty strict NetStr over S
the carrier of c₃ is non empty set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is non empty set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the carrier of (x "/\" c₃) is non empty set
the InternalRel of (x "/\" c₃) is Relation-like the carrier of (x "/\" c₃) -defined the carrier of (x "/\" c₃) -valued Element of K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)))
K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)) is non empty set
K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c₃), the InternalRel of (x "/\" c₃) #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty transitive NetStr over S
x "/\" c₃ is non empty strict NetStr over S
the carrier of c₃ is non empty set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is non empty set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the carrier of (x "/\" c₃) is non empty set
the InternalRel of (x "/\" c₃) is Relation-like the carrier of (x "/\" c₃) -defined the carrier of (x "/\" c₃) -valued Element of K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)))
K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃)) is non empty set
K10(K11( the carrier of (x "/\" c₃), the carrier of (x "/\" c₃))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c₃), the InternalRel of (x "/\" c₃) #) is strict RelStr
x is set
S is non empty RelStr
the carrier of S is non empty set
K11(x, the carrier of S) is set
K10(K11(x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like x -defined the carrier of S -valued Function-like V34(x) V36(x, the carrier of S) Element of K10(K11(x, the carrier of S))
FinSups c₃ is non empty directed NetStr over S
the carrier of (FinSups c₃) is non empty set
d is Element of the carrier of (FinSups c₃)
X is Element of the carrier of (FinSups c₃)
xM is Element of the carrier of (FinSups c₃)
Fin x is non empty cup-closed diff-closed preBoolean set
K11((Fin x), the carrier of S) is non empty set
K10(K11((Fin x), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelIncl (Fin x) is Relation-like Fin x -defined Fin x -valued reflexive antisymmetric transitive V34( Fin x) V36( Fin x, Fin x) Element of K10(K11((Fin x),(Fin x)))
K11((Fin x),(Fin x)) is non empty set
K10(K11((Fin x),(Fin x))) is non empty cup-closed diff-closed preBoolean set
InclPoset (Fin x) is strict RelStr
RelStr(# (Fin x),(RelIncl (Fin x)) #) is strict RelStr
the carrier of (InclPoset (Fin x)) is set
M is non empty Relation-like Fin x -defined the carrier of S -valued Function-like V34( Fin x) V36( Fin x, the carrier of S) Element of K10(K11((Fin x), the carrier of S))
NetStr(# (Fin x),(RelIncl (Fin x)),M #) is non empty strict NetStr over S
x is Element of the carrier of (InclPoset (Fin x))
A is Element of the carrier of (InclPoset (Fin x))
M is non empty Relation-like Fin x -defined the carrier of S -valued Function-like V34( Fin x) V36( Fin x, the carrier of S) Element of K10(K11((Fin x), the carrier of S))
NetStr(# (Fin x),(RelIncl (Fin x)),M #) is non empty strict NetStr over S
x is Element of the carrier of (InclPoset (Fin x))
M is non empty Relation-like Fin x -defined the carrier of S -valued Function-like V34( Fin x) V36( Fin x, the carrier of S) Element of K10(K11((Fin x), the carrier of S))
NetStr(# (Fin x),(RelIncl (Fin x)),M #) is non empty strict NetStr over S
M is non empty Relation-like Fin x -defined the carrier of S -valued Function-like V34( Fin x) V36( Fin x, the carrier of S) Element of K10(K11((Fin x), the carrier of S))
NetStr(# (Fin x),(RelIncl (Fin x)),M #) is non empty strict NetStr over S
S is non empty RelStr
x is NetStr over S
the mapping of x is Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is set
the carrier of S is non empty set
K11( the carrier of x, the carrier of S) is set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
//\ ( the mapping of x,S) is Element of the carrier of S
S is 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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
NetStr(# the carrier of S, the InternalRel of S,(id S) #) is strict NetStr over S
the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #) is set
the InternalRel of NetStr(# the carrier of S, the InternalRel of S,(id S) #) is Relation-like the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #) -defined the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #) -valued Element of K10(K11( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #)))
K11( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #)) is set
K10(K11( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the InternalRel of NetStr(# the carrier of S, the InternalRel of S,(id S) #) #) is strict RelStr
the mapping of NetStr(# the carrier of S, the InternalRel of S,(id S) #) is Relation-like the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #) -defined the carrier of S -valued Function-like V36( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of S) Element of K10(K11( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of S))
K11( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of S) is set
K10(K11( the carrier of NetStr(# the carrier of S, the InternalRel of S,(id S) #), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is strict NetStr over S
the carrier of x is set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the mapping of x is Relation-like the carrier of x -defined the carrier of S -valued Function-like V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
c₃ is strict NetStr over S
the carrier of c₃ is set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c₃, the InternalRel of c₃ #) is strict RelStr
the mapping of c₃ is Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
K11( the carrier of c₃, the carrier of S) is set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
S is non empty RelStr
(S) is strict NetStr over S
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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict 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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
S is reflexive RelStr
(S) is strict NetStr over S
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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict 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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
S is antisymmetric RelStr
(S) is strict NetStr over S
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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict 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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
S is transitive RelStr
(S) is strict NetStr over S
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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict 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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
S is non empty with_suprema RelStr
(S) is non empty strict NetStr over S
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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean 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 Element of K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is non empty set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
[#] S is non empty non proper directed lower upper Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
[#] (S) is non empty non proper lower upper Element of K10( the carrier of (S))
K10( the carrier of (S)) is non empty cup-closed diff-closed preBoolean set
S is directed RelStr
(S) is strict NetStr over S
[#] S is non proper Element of K10( the carrier of S)
the carrier of S is set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of S, the InternalRel of S #) is strict 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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
[#] (S) is non proper Element of K10( the carrier of (S))
K10( the carrier of (S)) is non empty cup-closed diff-closed preBoolean set
S is non empty RelStr
(S) is non empty strict NetStr over S
the carrier of (S) is non empty set
the carrier of S is non empty set
netmap ((S),S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
K11( the carrier of (S), the carrier of S) is non empty set
K10(K11( the carrier of (S), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) monotone Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is non empty set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean 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 Element of K10(K11( the carrier of S, the carrier of S))
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
c₃ is Element of the carrier of (S)
(S) . c₃ is Element of the carrier of S
the mapping of (S) . c₃ is Element of the carrier of S
d is Element of the carrier of (S)
X is Element of the carrier of (S)
(S) . X is Element of the carrier of S
the mapping of (S) . X is Element of the carrier of S
the mapping of (S) . c₃ is Element of the carrier of S
the mapping of (S) . X 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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) is strict NetStr over S
the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) is set
the InternalRel of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) is Relation-like the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) -defined the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) -valued Element of K10(K11( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #)))
K11( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #)) is set
K10(K11( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #))) is non empty cup-closed diff-closed preBoolean set
the mapping of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) is Relation-like the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #) -defined the carrier of S -valued Function-like V36( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of S) Element of K10(K11( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of S))
K11( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of S) is set
K10(K11( the carrier of NetStr(# the carrier of S,( the InternalRel of S ~),(id S) #), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is strict NetStr over S
the carrier of x is set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the mapping of x is Relation-like the carrier of x -defined the carrier of S -valued Function-like V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
c₃ is strict NetStr over S
the carrier of c₃ is set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of K10(K11( the carrier of c₃, the carrier of c₃))
K11( the carrier of c₃, the carrier of c₃) is set
K10(K11( the carrier of c₃, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
the mapping of c₃ is Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
K11( the carrier of c₃, the carrier of S) is set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
S is RelStr
S ~ is strict 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 K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
RelStr(# the carrier of S,( the InternalRel of S ~) #) is strict 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 K10(K11( the carrier of (S ~), the carrier of (S ~)))
K11( the carrier of (S ~), the carrier of (S ~)) is set
K10(K11( the carrier of (S ~), the carrier of (S ~))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S ~), the InternalRel of (S ~) #) is strict RelStr
(S) is strict NetStr over S
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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
S is non empty RelStr
(S) is strict NetStr over S
S ~ is non empty 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 Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
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 Element of K10(K11( the carrier of (S ~), the carrier of (S ~)))
K11( the carrier of (S ~), the carrier of (S ~)) is non empty set
K10(K11( the carrier of (S ~), the carrier of (S ~))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S ~), the InternalRel of (S ~) #) is strict 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 K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
S is reflexive RelStr
(S) is strict NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the carrier of S is set
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
the carrier of (S) is set
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
S is antisymmetric RelStr
(S) is strict NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the carrier of S is set
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
the carrier of (S) is set
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
S is transitive RelStr
(S) is strict NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the carrier of S is set
K11( the carrier of S, the carrier of S) is set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
the carrier of (S) is set
K11( the carrier of (S), the carrier of (S)) is set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
S is non empty with_infima RelStr
(S) is non empty strict NetStr over S
S ~ is non empty 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 Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
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 Element of K10(K11( the carrier of (S ~), the carrier of (S ~)))
K11( the carrier of (S ~), the carrier of (S ~)) is non empty set
K10(K11( the carrier of (S ~), the carrier of (S ~))) is non empty cup-closed diff-closed preBoolean 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 Element of K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is non empty set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr
x is non empty with_suprema RelStr
[#] x is non empty non proper directed lower upper Element of K10( the carrier of x)
the carrier of x is non empty set
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
[#] (S) is non empty non proper lower upper Element of K10( the carrier of (S))
K10( the carrier of (S)) is non empty cup-closed diff-closed preBoolean set
S is non empty RelStr
(S) is non empty strict NetStr over S
S ~ is non empty 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 Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
RelStr(# the carrier of S,( the InternalRel of S ~) #) is strict RelStr
the carrier of (S ~) is non empty set
K11( the carrier of (S ~), the carrier of S) is non empty set
K10(K11( the carrier of (S ~), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) monotone Element of K10(K11( the carrier of S, the carrier of S))
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of (S ~)) is non empty set
K10(K11( the carrier of S, the carrier of (S ~))) is non empty cup-closed diff-closed preBoolean set
c₃ is non empty Relation-like the carrier of (S ~) -defined the carrier of S -valued Function-like V34( the carrier of (S ~)) V36( the carrier of (S ~), the carrier of S) Element of K10(K11( the carrier of (S ~), the carrier of S))
d is non empty Relation-like the carrier of S -defined the carrier of (S ~) -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of (S ~)) Element of K10(K11( the carrier of S, the carrier of (S ~)))
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the carrier of (S) is non empty set
netmap ((S),S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
K11( the carrier of (S), the carrier of S) is non empty set
K10(K11( the carrier of (S), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is non empty set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean 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 Element of K10(K11( the carrier of (S ~), the carrier of (S ~)))
K11( the carrier of (S ~), the carrier of (S ~)) is non empty set
K10(K11( the carrier of (S ~), the carrier of (S ~))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S ~), the InternalRel of (S ~) #) is strict RelStr
the carrier of (S) is non empty set
c₃ is Element of the carrier of (S)
(S) . c₃ is Element of the carrier of S
the carrier of S is non empty set
the mapping of (S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
K11( the carrier of (S), the carrier of S) is non empty set
K10(K11( the carrier of (S), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S) . c₃ is Element of the carrier of S
d is Element of the carrier of (S)
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) monotone Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is non empty set
K10(K11( the carrier of (S), the carrier of (S))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
X is Element of the carrier of (S)
(S) . X is Element of the carrier of S
the mapping of (S) . X is Element of the carrier of S
[c₃,X] is V7() Element of K11( the carrier of (S), the carrier of (S))
{c₃,X} is non empty set
{c₃} is non empty trivial 1 -element set
{{c₃,X},{c₃}} is non empty set
[X,c₃] is V7() Element of K11( the carrier of (S), the carrier of (S))
{X,c₃} is non empty set
{X} is non empty trivial 1 -element set
{{X,c₃},{X}} is non empty set
the InternalRel of (S) ~ is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
xM is Element of the carrier of S
(id S) . xM is Element of the carrier of S
x is Element of the carrier of S
(id S) . x is Element of the carrier of S
S is non empty 1-sorted
x is non empty NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the carrier of S is non empty set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
d is set
X is set
K11(d, the carrier of S) is set
K10(K11(d, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x | d is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
the InternalRel of x |_2 d is Relation-like d -defined d -valued Element of K10(K11(d,d))
K11(d,d) is set
K10(K11(d,d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x /\ K11(d,d) is set
X is Relation-like d -defined the carrier of S -valued Function-like V34(d) V36(d, the carrier of S) Element of K10(K11(d, the carrier of S))
NetStr(# d,( the InternalRel of x |_2 d),X #) is strict NetStr over S
the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) is set
the InternalRel of NetStr(# d,( the InternalRel of x |_2 d),X #) is Relation-like the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) -defined the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) -valued Element of K10(K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #)))
K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #)) is set
K10(K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x |_2 the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) is Relation-like the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) -defined the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) -valued Element of K10(K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #)))
the InternalRel of x /\ K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #)) is set
the mapping of NetStr(# d,( the InternalRel of x |_2 d),X #) is Relation-like the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) -defined the carrier of S -valued Function-like V34( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #)) V36( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of S) Element of K10(K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of S))
K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of S) is set
K10(K11( the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x | the carrier of NetStr(# d,( the InternalRel of x |_2 d),X #) is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
x is set
A is Element of the carrier of x
x is set
d is strict NetStr over S
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x |_2 the carrier of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
the InternalRel of x /\ K11( the carrier of d, the carrier of d) is set
the mapping of d is Relation-like the carrier of d -defined the carrier of S -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of S) Element of K10(K11( the carrier of d, the carrier of S))
K11( the carrier of d, the carrier of S) is set
K10(K11( the carrier of d, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x | the carrier of d is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
X is strict NetStr over S
the carrier of X is set
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K10(K11( the carrier of X, the carrier of X))
K11( the carrier of X, the carrier of X) is set
K10(K11( the carrier of X, the carrier of X)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x |_2 the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K10(K11( the carrier of X, the carrier of X))
the InternalRel of x /\ K11( the carrier of X, the carrier of X) is set
the mapping of X is Relation-like the carrier of X -defined the carrier of S -valued Function-like V34( the carrier of X) V36( the carrier of X, the carrier of S) Element of K10(K11( the carrier of X, the carrier of S))
K11( the carrier of X, the carrier of S) is set
K10(K11( the carrier of X, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x | the carrier of X is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
S is non empty 1-sorted
x is non empty NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is strict NetStr over S
the carrier of (S,x,c₃) is set
{ b₁ where b₁ is Element of the carrier of x : c₃ <= b₁ } is set
d is set
X is Element of the carrier of x
d is set
X is Element of the carrier of x
S is non empty 1-sorted
x is non empty NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is strict NetStr over S
the carrier of (S,x,c₃) is set
d is set
X is Element of the carrier of x
S is non empty 1-sorted
x is non empty NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is strict NetStr over S
the mapping of (S,x,c₃) is Relation-like the carrier of (S,x,c₃) -defined the carrier of S -valued Function-like V34( the carrier of (S,x,c₃)) V36( the carrier of (S,x,c₃), the carrier of S) Element of K10(K11( the carrier of (S,x,c₃), the carrier of S))
the carrier of (S,x,c₃) is set
the carrier of S is non empty set
K11( the carrier of (S,x,c₃), the carrier of S) is set
K10(K11( the carrier of (S,x,c₃), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x | the carrier of (S,x,c₃) is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
the InternalRel of (S,x,c₃) is Relation-like the carrier of (S,x,c₃) -defined the carrier of (S,x,c₃) -valued Element of K10(K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃)))
K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃)) is set
K10(K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x |_2 the carrier of (S,x,c₃) is Relation-like the carrier of (S,x,c₃) -defined the carrier of (S,x,c₃) -valued Element of K10(K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃)))
the InternalRel of x /\ K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃)) is set
d is SubNetStr of x
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of x |_2 the carrier of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
the InternalRel of x /\ K11( the carrier of d, the carrier of d) is set
S is non empty 1-sorted
x is non empty reflexive NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is strict NetStr over S
d is non empty strict NetStr over S
the carrier of d is non empty set
X is Element of the carrier of d
xM is Element of the carrier of x
S is non empty 1-sorted
x is non empty directed NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is strict NetStr over S
d is Element of the carrier of x
S is non empty 1-sorted
x is non empty reflexive antisymmetric NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty reflexive strict NetStr over S
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of (S,x,c₃)
X is Element of the carrier of (S,x,c₃)
xM is Element of the carrier of x
x is Element of the carrier of x
S is non empty 1-sorted
x is non empty antisymmetric directed NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty strict NetStr over S
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of (S,x,c₃)
X is Element of the carrier of (S,x,c₃)
xM is Element of the carrier of x
x is Element of the carrier of x
S is non empty 1-sorted
x is non empty reflexive transitive NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty reflexive strict NetStr over S
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of (S,x,c₃)
X is Element of the carrier of (S,x,c₃)
xM is Element of the carrier of (S,x,c₃)
x is Element of the carrier of x
x is Element of the carrier of x
A is Element of the carrier of x
S is non empty 1-sorted
x is non empty transitive directed NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty strict NetStr over S
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of (S,x,c₃)
X is Element of the carrier of (S,x,c₃)
xM is Element of the carrier of (S,x,c₃)
x is Element of the carrier of x
x is Element of the carrier of x
A is Element of the carrier of x
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of (S,x,c₃)
X is Element of the carrier of (S,x,c₃)
xM is Element of the carrier of x
x is Element of the carrier of x
x is Element of the carrier of x
A is Element of the carrier of (S,x,c₃)
S is non empty 1-sorted
x is non empty reflexive NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty reflexive strict NetStr over S
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of x
x . d is Element of the carrier of S
the carrier of S is non empty set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . d is Element of the carrier of S
X is Element of the carrier of (S,x,c₃)
(S,x,c₃) . X is Element of the carrier of S
the mapping of (S,x,c₃) is non empty Relation-like the carrier of (S,x,c₃) -defined the carrier of S -valued Function-like V34( the carrier of (S,x,c₃)) V36( the carrier of (S,x,c₃), the carrier of S) Element of K10(K11( the carrier of (S,x,c₃), the carrier of S))
K11( the carrier of (S,x,c₃), the carrier of S) is non empty set
K10(K11( the carrier of (S,x,c₃), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S,x,c₃) . X is Element of the carrier of S
the mapping of x | the carrier of (S,x,c₃) is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
( the mapping of x | the carrier of (S,x,c₃)) . X is set
S is non empty 1-sorted
x is non empty directed NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty strict NetStr over S
the carrier of (S,x,c₃) is non empty set
d is Element of the carrier of x
x . d is Element of the carrier of S
the carrier of S is non empty set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . d is Element of the carrier of S
X is Element of the carrier of (S,x,c₃)
(S,x,c₃) . X is Element of the carrier of S
the mapping of (S,x,c₃) is non empty Relation-like the carrier of (S,x,c₃) -defined the carrier of S -valued Function-like V34( the carrier of (S,x,c₃)) V36( the carrier of (S,x,c₃), the carrier of S) Element of K10(K11( the carrier of (S,x,c₃), the carrier of S))
K11( the carrier of (S,x,c₃), the carrier of S) is non empty set
K10(K11( the carrier of (S,x,c₃), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S,x,c₃) . X is Element of the carrier of S
the mapping of x | the carrier of (S,x,c₃) is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
( the mapping of x | the carrier of (S,x,c₃)) . X is set
S is non empty 1-sorted
x is non empty transitive directed NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty transitive strict directed NetStr over S
d is non empty transitive directed NetStr over S
the carrier of d is non empty set
K11( the carrier of d, the carrier of x) is non empty set
K10(K11( the carrier of d, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
id the carrier of d is non empty Relation-like the carrier of d -defined the carrier of d -valued Function-like one-to-one V34( the carrier of d) V36( the carrier of d, the carrier of d) Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is non empty set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
X is non empty Relation-like the carrier of d -defined the carrier of x -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of x) Element of K10(K11( the carrier of d, the carrier of x))
the carrier of S is non empty set
the mapping of d is non empty Relation-like the carrier of d -defined the carrier of S -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of S) Element of K10(K11( the carrier of d, the carrier of S))
K11( the carrier of d, the carrier of S) is non empty set
K10(K11( the carrier of d, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x * X is non empty Relation-like the carrier of d -defined the carrier of S -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of S) Element of K10(K11( the carrier of d, the carrier of S))
xM is set
the mapping of d . xM is set
( the mapping of x * X) . xM is set
the mapping of x | the carrier of d is Relation-like the carrier of x -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of x, the carrier of S))
( the mapping of x | the carrier of d) . xM is set
the mapping of x . xM is set
X . xM is set
the mapping of x . (X . xM) is set
xM is Element of the carrier of x
x is Element of the carrier of x
x is Element of the carrier of d
A is Element of the carrier of d
X . A is Element of the carrier of x
M is Element of the carrier of x
S is non empty 1-sorted
x is non empty transitive directed NetStr over S
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of S is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) is non empty strict NetStr over S
the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) is non empty set
the InternalRel of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) is Relation-like the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) -defined the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) -valued Element of K10(K11( the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #), the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #)))
K11( the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #), the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #)) is non empty set
K10(K11( the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #), the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #), the InternalRel of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) #) is strict RelStr
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
[#] x is non empty non proper lower upper Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
[#] NetStr(# the carrier of x, the InternalRel of x, the mapping of x #) is non empty non proper lower upper Element of K10( the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #))
K10( the carrier of NetStr(# the carrier of x, the InternalRel of x, the mapping of x #)) is non empty cup-closed diff-closed preBoolean set
d is non empty transitive directed NetStr over S
the carrier of d is non empty set
K11( the carrier of d, the carrier of x) is non empty set
K10(K11( the carrier of d, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
id x is non empty Relation-like the carrier of x -defined the carrier of x -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of x) monotone Element of K10(K11( the carrier of x, the carrier of x))
id the carrier of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Function-like one-to-one V34( the carrier of x) V36( the carrier of x, the carrier of x) Element of K10(K11( the carrier of x, the carrier of x))
X is non empty Relation-like the carrier of d -defined the carrier of x -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of x) Element of K10(K11( the carrier of d, the carrier of x))
the mapping of d is non empty Relation-like the carrier of d -defined the carrier of S -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of S) Element of K10(K11( the carrier of d, the carrier of S))
K11( the carrier of d, the carrier of S) is non empty set
K10(K11( the carrier of d, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x * X is non empty Relation-like the carrier of d -defined the carrier of S -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of S) Element of K10(K11( the carrier of d, the carrier of S))
xM is Element of the carrier of x
x is Element of the carrier of d
x is Element of the carrier of d
X . x is Element of the carrier of x
X is non empty transitive directed subnet of x
S is non empty 1-sorted
x is non empty transitive directed NetStr over S
the carrier of x is non empty set
c₃ is Element of the carrier of x
(S,x,c₃) is non empty transitive strict directed NetStr over S
S is non empty 1-sorted
the carrier of S is non empty set
x is 1-sorted
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
d is NetStr over S
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
the mapping of d is Relation-like the carrier of d -defined the carrier of S -valued Function-like V34( the carrier of d) V36( the carrier of d, the carrier of S) Element of K10(K11( the carrier of d, the carrier of S))
K11( the carrier of d, the carrier of S) is set
K10(K11( the carrier of d, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
c₃ * the mapping of d is Relation-like the carrier of d -defined the carrier of x -valued Function-like V36( the carrier of d, the carrier of x) Element of K10(K11( the carrier of d, the carrier of x))
K11( the carrier of d, the carrier of x) is set
K10(K11( the carrier of d, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) is strict NetStr over x
the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) is set
the InternalRel of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) is Relation-like the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) -defined the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) -valued Element of K10(K11( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #)))
K11( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #)) is set
K10(K11( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the InternalRel of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) #) is strict RelStr
the mapping of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) is Relation-like the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #) -defined the carrier of x -valued Function-like V36( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of x) Element of K10(K11( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of x))
K11( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of x) is set
K10(K11( the carrier of NetStr(# the carrier of d, the InternalRel of d,(c₃ * the mapping of d) #), the carrier of x)) is non empty cup-closed diff-closed preBoolean set
X is strict NetStr over x
the carrier of X is set
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K10(K11( the carrier of X, the carrier of X))
K11( the carrier of X, the carrier of X) is set
K10(K11( the carrier of X, the carrier of X)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
the mapping of X is Relation-like the carrier of X -defined the carrier of x -valued Function-like V36( the carrier of X, the carrier of x) Element of K10(K11( the carrier of X, the carrier of x))
K11( the carrier of X, the carrier of x) is set
K10(K11( the carrier of X, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
xM is strict NetStr over x
the carrier of xM is set
the InternalRel of xM is Relation-like the carrier of xM -defined the carrier of xM -valued Element of K10(K11( the carrier of xM, the carrier of xM))
K11( the carrier of xM, the carrier of xM) is set
K10(K11( the carrier of xM, the carrier of xM)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of xM, the InternalRel of xM #) is strict RelStr
the mapping of xM is Relation-like the carrier of xM -defined the carrier of x -valued Function-like V36( the carrier of xM, the carrier of x) Element of K10(K11( the carrier of xM, the carrier of x))
K11( the carrier of xM, the carrier of x) is set
K10(K11( the carrier of xM, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
S is non empty 1-sorted
the carrier of S is non empty set
x is 1-sorted
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
d is non empty NetStr over S
(S,x,c₃,d) is strict NetStr over x
the carrier of d is non empty set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is non empty set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
the carrier of (S,x,c₃,d) is set
the InternalRel of (S,x,c₃,d) is Relation-like the carrier of (S,x,c₃,d) -defined the carrier of (S,x,c₃,d) -valued Element of K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)))
K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)) is set
K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,x,c₃,d), the InternalRel of (S,x,c₃,d) #) is strict RelStr
S is non empty 1-sorted
the carrier of S is non empty set
x is 1-sorted
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
d is reflexive NetStr over S
(S,x,c₃,d) is strict NetStr over x
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
the carrier of (S,x,c₃,d) is set
the InternalRel of (S,x,c₃,d) is Relation-like the carrier of (S,x,c₃,d) -defined the carrier of (S,x,c₃,d) -valued Element of K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)))
K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)) is set
K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,x,c₃,d), the InternalRel of (S,x,c₃,d) #) is strict RelStr
S is non empty 1-sorted
the carrier of S is non empty set
x is 1-sorted
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
d is antisymmetric NetStr over S
(S,x,c₃,d) is strict NetStr over x
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
the carrier of (S,x,c₃,d) is set
the InternalRel of (S,x,c₃,d) is Relation-like the carrier of (S,x,c₃,d) -defined the carrier of (S,x,c₃,d) -valued Element of K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)))
K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)) is set
K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,x,c₃,d), the InternalRel of (S,x,c₃,d) #) is strict RelStr
S is non empty 1-sorted
the carrier of S is non empty set
x is 1-sorted
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
d is transitive NetStr over S
(S,x,c₃,d) is strict NetStr over x
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
the carrier of (S,x,c₃,d) is set
the InternalRel of (S,x,c₃,d) is Relation-like the carrier of (S,x,c₃,d) -defined the carrier of (S,x,c₃,d) -valued Element of K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)))
K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)) is set
K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,x,c₃,d), the InternalRel of (S,x,c₃,d) #) is strict RelStr
S is non empty 1-sorted
the carrier of S is non empty set
x is 1-sorted
the carrier of x is set
K11( the carrier of S, the carrier of x) is set
K10(K11( the carrier of S, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c₃ is Relation-like the carrier of S -defined the carrier of x -valued Function-like V36( the carrier of S, the carrier of x) Element of K10(K11( the carrier of S, the carrier of x))
d is directed NetStr over S
(S,x,c₃,d) is strict NetStr over x
the carrier of d is set
the InternalRel of d is Relation-like the carrier of d -defined the carrier of d -valued Element of K10(K11( the carrier of d, the carrier of d))
K11( the carrier of d, the carrier of d) is set
K10(K11( the carrier of d, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of d, the InternalRel of d #) is strict RelStr
the carrier of (S,x,c₃,d) is set
the InternalRel of (S,x,c₃,d) is Relation-like the carrier of (S,x,c₃,d) -defined the carrier of (S,x,c₃,d) -valued Element of K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)))
K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d)) is set
K10(K11( the carrier of (S,x,c₃,d), the carrier of (S,x,c₃,d))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,x,c₃,d), the InternalRel of (S,x,c₃,d) #) is strict RelStr
[#] d is non proper Element of K10( the carrier of d)
K10( the carrier of d) is non empty cup-closed diff-closed preBoolean set
[#] (S,x,c₃,d) is non proper Element of K10( the carrier of (S,x,c₃,d))
K10( the carrier of (S,x,c₃,d)) is non empty cup-closed diff-closed preBoolean set
S is non empty RelStr
the carrier of S is non empty set
x is non empty NetStr over S
c₃ is Element of the carrier of S
c₃ "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
(S,S,(c₃ "/\"),x) is non empty strict NetStr over S
c₃ "/\" x is non empty strict NetStr over S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the carrier of (S,S,(c₃ "/\"),x) is non empty set
the InternalRel of (S,S,(c₃ "/\"),x) is Relation-like the carrier of (S,S,(c₃ "/\"),x) -defined the carrier of (S,S,(c₃ "/\"),x) -valued Element of K10(K11( the carrier of (S,S,(c₃ "/\"),x), the carrier of (S,S,(c₃ "/\"),x)))
K11( the carrier of (S,S,(c₃ "/\"),x), the carrier of (S,S,(c₃ "/\"),x)) is non empty set
K10(K11( the carrier of (S,S,(c₃ "/\"),x), the carrier of (S,S,(c₃ "/\"),x))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,S,(c₃ "/\"),x), the InternalRel of (S,S,(c₃ "/\"),x) #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the carrier of (c₃ "/\" x) is non empty set
the InternalRel of (c₃ "/\" x) is Relation-like the carrier of (c₃ "/\" x) -defined the carrier of (c₃ "/\" x) -valued Element of K10(K11( the carrier of (c₃ "/\" x), the carrier of (c₃ "/\" x)))
K11( the carrier of (c₃ "/\" x), the carrier of (c₃ "/\" x)) is non empty set
K10(K11( the carrier of (c₃ "/\" x), the carrier of (c₃ "/\" x))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (c₃ "/\" x), the InternalRel of (c₃ "/\" x) #) is strict RelStr
the mapping of (c₃ "/\" x) is non empty Relation-like the carrier of (c₃ "/\" x) -defined the carrier of S -valued Function-like V34( the carrier of (c₃ "/\" x)) V36( the carrier of (c₃ "/\" x), the carrier of S) Element of K10(K11( the carrier of (c₃ "/\" x), the carrier of S))
K11( the carrier of (c₃ "/\" x), the carrier of S) is non empty set
K10(K11( the carrier of (c₃ "/\" x), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
(c₃ "/\") * the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
X is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
xM is Element of the carrier of x
((c₃ "/\") * the mapping of x) . xM is Element of the carrier of S
X . xM is Element of the carrier of S
the mapping of x . xM is Element of the carrier of S
x is Element of the carrier of S
c₃ "/\" x is Element of the carrier of S
(c₃ "/\") . x is Element of the carrier of S
the mapping of (S,S,(c₃ "/\"),x) is non empty Relation-like the carrier of (S,S,(c₃ "/\"),x) -defined the carrier of S -valued Function-like V34( the carrier of (S,S,(c₃ "/\"),x)) V36( the carrier of (S,S,(c₃ "/\"),x), the carrier of S) Element of K10(K11( the carrier of (S,S,(c₃ "/\"),x), the carrier of S))
K11( the carrier of (S,S,(c₃ "/\"),x), the carrier of S) is non empty set
K10(K11( the carrier of (S,S,(c₃ "/\"),x), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
S is TopStruct
the carrier of S is set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is TopStruct
the carrier of x is set
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the topology of S is open Element of K10(K10( the carrier of S))
TopStruct(# the carrier of S, the topology of S #) is strict TopStruct
the topology of x is open Element of K10(K10( the carrier of x))
TopStruct(# the carrier of x, the topology of x #) is strict TopStruct
c₃ is Element of K10(K10( the carrier of S))
d is Element of K10(K10( the carrier of x))
X is Element of K10( the carrier of x)
xM is Element of K10( the carrier of S)
S is TopStruct
the carrier of S is set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is TopStruct
the carrier of x is set
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of x)) is non empty cup-closed diff-closed preBoolean set
the topology of S is open Element of K10(K10( the carrier of S))
TopStruct(# the carrier of S, the topology of S #) is strict TopStruct
the topology of x is open Element of K10(K10( the carrier of x))
TopStruct(# the carrier of x, the topology of x #) is strict TopStruct
c₃ is Element of K10(K10( the carrier of S))
d is Element of K10(K10( the carrier of x))
X is Element of K10( the carrier of x)
xM is Element of K10( the carrier of S)
[#] S is non proper dense Element of K10( the carrier of S)
([#] S) \ xM is Element of K10( the carrier of S)
[#] x is non proper dense Element of K10( the carrier of x)
([#] x) \ X is Element of K10( the carrier of x)
S is non empty set
K11(S,S) is non empty set
K10(K11(S,S)) is non empty cup-closed diff-closed preBoolean set
K10(S) is non empty cup-closed diff-closed preBoolean set
K10(K10(S)) is non empty cup-closed diff-closed preBoolean set
x is Relation-like S -defined S -valued Element of K10(K11(S,S))
c₃ is Element of K10(K10(S))
(S,x,c₃) is () ()
S is set
{S} is non empty trivial 1 -element set
K11({S},{S}) is non empty set
K10(K11({S},{S})) is non empty cup-closed diff-closed preBoolean set
K10({S}) is non empty cup-closed diff-closed preBoolean set
K10(K10({S})) is non empty cup-closed diff-closed preBoolean set
x is Relation-like {S} -defined {S} -valued Element of K10(K11({S},{S}))
c₃ is Element of K10(K10({S}))
({S},x,c₃) is non empty () ()
the carrier of ({S},x,c₃) is non empty set
S is set
K11(S,S) is set
K10(K11(S,S)) is non empty cup-closed diff-closed preBoolean set
K10(S) is non empty cup-closed diff-closed preBoolean set
K10(K10(S)) is non empty cup-closed diff-closed preBoolean set
x is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) V36(S,S) Element of K10(K11(S,S))
c₃ is Element of K10(K10(S))
(S,x,c₃) is () ()
the InternalRel of (S,x,c₃) is Relation-like the carrier of (S,x,c₃) -defined the carrier of (S,x,c₃) -valued Element of K10(K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃)))
the carrier of (S,x,c₃) is set
K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃)) is set
K10(K11( the carrier of (S,x,c₃), the carrier of (S,x,c₃))) is non empty cup-closed diff-closed preBoolean set
field the InternalRel of (S,x,c₃) is set
0 is empty Function-like functional V39() V40() V41() V43() V44() V45() finite cardinal {} -element Element of K160()
{0} is non empty trivial 1 -element Element of K10(K160())
K10({0}) is non empty cup-closed diff-closed preBoolean set
K10(K10({0})) is non empty cup-closed diff-closed preBoolean set
K11({0},{0}) is non empty set
K10(K11({0},{0})) is non empty cup-closed diff-closed preBoolean set
{{},{0}} is non empty set
K11(K160(),K160()) is non empty non finite set
[0,0] is V7() Element of K11(K160(),K160())
{0,0} is non empty set
{0} is non empty trivial 1 -element set
{{0,0},{0}} is non empty set
{[0,0]} is non empty trivial Relation-like K160() -defined K160() -valued Function-like constant 1 -element Element of K10(K11(K160(),K160()))
K10(K11(K160(),K160())) is non empty cup-closed diff-closed preBoolean non finite set
S is Element of K10(K10({0}))
x is Relation-like {0} -defined {0} -valued Element of K10(K11({0},{0}))
({0},x,S) is non empty trivial finite 1 -element () ()
the carrier of ({0},x,S) is non empty trivial finite 1 -element set
d is Element of the carrier of ({0},x,S)
[d,d] is V7() Element of K11( the carrier of ({0},x,S), the carrier of ({0},x,S))
K11( the carrier of ({0},x,S), the carrier of ({0},x,S)) is non empty set
{d,d} is non empty set
{d} is non empty trivial 1 -element set
{{d,d},{d}} is non empty set
the topology of ({0},x,S) is open Element of K10(K10( the carrier of ({0},x,S)))
the carrier of ({0},x,S) is non empty trivial finite 1 -element set
K10( the carrier of ({0},x,S)) is non empty cup-closed diff-closed preBoolean set
K10(K10( the carrier of ({0},x,S))) is non empty cup-closed diff-closed preBoolean set
bool the carrier of ({0},x,S) is non empty cup-closed diff-closed preBoolean Element of K10(K10( the carrier of ({0},x,S)))
bool {0} is non empty cup-closed diff-closed preBoolean Element of K10(K10({0}))
S is Relation-like {0} -defined {0} -valued Element of K10(K11({0},{0}))
x is Element of K10(K10({0}))
({0},S,x) is non empty trivial finite 1 -element () ()
bool {0} is non empty cup-closed diff-closed preBoolean Element of K10(K10({0}))
x is Relation-like {0} -defined {0} -valued Element of K10(K11({0},{0}))
S is Element of K10(K10({0}))
({0},x,S) is non empty trivial finite 1 -element () ()
c₃ is non empty trivial finite 1 -element TopSpace-like discrete V113() V114() V115() reflexive transitive antisymmetric lower-bounded upper-bounded bounded connected up-complete /\-complete distributive V221() complemented with_suprema with_infima V248() satisfying_MC meet-continuous compact ()
d is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ()
the carrier of d is non empty set
X is Element of the carrier of d
xM is Element of the carrier of d
K10( the carrier of d) is non empty cup-closed diff-closed preBoolean set
S is non empty TopSpace-like T_0 T_1 T_2 TopStruct
x is non empty TopSpace-like T_0 T_1 T_2 SubSpace of S
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
x is Element of the carrier of S
OpenNeighborhoods x is non empty transitive directed RelStr
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } is strict RelStr
(InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~ is strict RelStr
the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) is set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )))
K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )) is set
K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~ is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )))
RelStr(# the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ),( the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~) #) is strict RelStr
the carrier of (OpenNeighborhoods x) is non empty set
c₃ is Element of the carrier of (OpenNeighborhoods x)
d is Element of K10( the carrier of S)
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
x is Element of the carrier of S
OpenNeighborhoods x is non empty transitive directed RelStr
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } is strict RelStr
(InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~ is strict RelStr
the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) is set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )))
K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )) is set
K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~ is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )))
RelStr(# the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ),( the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~) #) is strict RelStr
the carrier of (OpenNeighborhoods x) is non empty set
c₃ is Element of the carrier of (OpenNeighborhoods x)
d is Element of the carrier of (OpenNeighborhoods x)
c₃ /\ d is set
X is Element of K10( the carrier of S)
xM is Element of K10( the carrier of S)
X /\ xM is Element of K10( the carrier of S)
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
x is Element of the carrier of S
OpenNeighborhoods x is non empty transitive directed RelStr
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } is strict RelStr
(InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~ is strict RelStr
the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) is set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )))
K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )) is set
K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~ is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } )))
RelStr(# the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ),( the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( x in b₁ & b₁ is open ) } ) ~) #) is strict RelStr
the carrier of (OpenNeighborhoods x) is non empty set
c₃ is Element of the carrier of (OpenNeighborhoods x)
d is Element of the carrier of (OpenNeighborhoods x)
c₃ \/ d is set
X is Element of K10( the carrier of S)
xM is Element of K10( the carrier of S)
X \/ xM is Element of K10( the carrier of S)
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of S
c₃ is non empty transitive directed NetStr over S
Lim c₃ is Element of K10( the carrier of S)
the mapping of c₃ is non empty Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
the carrier of c₃ is non empty set
K11( the carrier of c₃, the carrier of S) is non empty set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of c₃ is Element of K10( the carrier of S)
d is Element of K10( the carrier of S)
Cl d is closed Element of K10( the carrier of S)
X is Element of K10( the carrier of S)
Int X is open Element of K10( the carrier of S)
xM is a_neighborhood of x
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima ()
the carrier of S is non empty set
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
x is non empty transitive directed convergent NetStr over S
lim x is Element of the carrier of S
c₃ is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
c₃ . (lim x) is Element of the carrier of S
(S,S,c₃,x) is non empty transitive strict directed NetStr over S
Lim (S,S,c₃,x) is trivial Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
d is a_neighborhood of c₃ . (lim x)
dom c₃ is Element of K10( the carrier of S)
X is a_neighborhood of lim x
c₃ .: X is Element of K10( the carrier of S)
Lim x is trivial Element of K10( the carrier of S)
the carrier of x is non empty set
xM is Element of the carrier of x
the carrier of (S,S,c₃,x) is non empty set
the InternalRel of (S,S,c₃,x) is Relation-like the carrier of (S,S,c₃,x) -defined the carrier of (S,S,c₃,x) -valued Element of K10(K11( the carrier of (S,S,c₃,x), the carrier of (S,S,c₃,x)))
K11( the carrier of (S,S,c₃,x), the carrier of (S,S,c₃,x)) is non empty set
K10(K11( the carrier of (S,S,c₃,x), the carrier of (S,S,c₃,x))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (S,S,c₃,x), the InternalRel of (S,S,c₃,x) #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))
K11( the carrier of x, the carrier of x) is non empty set
K10(K11( the carrier of x, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
x is Element of the carrier of (S,S,c₃,x)
x is Element of the carrier of (S,S,c₃,x)
(S,S,c₃,x) . x is Element of the carrier of S
the mapping of (S,S,c₃,x) is non empty Relation-like the carrier of (S,S,c₃,x) -defined the carrier of S -valued Function-like V34( the carrier of (S,S,c₃,x)) V36( the carrier of (S,S,c₃,x), the carrier of S) Element of K10(K11( the carrier of (S,S,c₃,x), the carrier of S))
K11( the carrier of (S,S,c₃,x), the carrier of S) is non empty set
K10(K11( the carrier of (S,S,c₃,x), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S,S,c₃,x) . x is Element of the carrier of S
A is Element of the carrier of x
x . A is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . A is Element of the carrier of S
c₃ . (x . A) is Element of the carrier of S
dom the mapping of x is Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
c₃ * the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
(c₃ * the mapping of x) . x is set
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima ()
the carrier of S is non empty set
x is non empty transitive directed convergent NetStr over S
lim x is Element of the carrier of S
c₃ is Element of the carrier of S
c₃ "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
c₃ "/\" (lim x) is Element of the carrier of S
c₃ "/\" x is non empty transitive strict directed NetStr over S
Lim (c₃ "/\" x) is trivial Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
(c₃ "/\") . (lim x) is Element of the carrier of S
(S,S,(c₃ "/\"),x) is non empty transitive strict directed NetStr over S
Lim (S,S,(c₃ "/\"),x) is trivial Element of K10( the carrier of S)
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima ()
the carrier of S is non empty set
x is Element of the carrier of S
uparrow x is non empty filtered upper Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
uparrow {x} is non empty upper Element of K10( the carrier of S)
x "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
(x "/\") " {x} is Element of K10( the carrier of S)
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is Element of the carrier of S
downarrow x is non empty directed lower Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
downarrow {x} is non empty lower Element of K10( the carrier of S)
x "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng (x "/\") is Element of K10( the carrier of S)
(rng (x "/\")) |` (x "/\") is Relation-like the carrier of S -defined the carrier of S -valued Function-like Element of K10(K11( the carrier of S, the carrier of S))
dom (x "/\") is Element of K10( the carrier of S)
[#] S is non empty non proper open closed dense non boundary directed filtered lower upper Element of K10( the carrier of S)
{x} "/\" ([#] S) is non empty Element of K10( the carrier of S)
{ (x "/\" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of S : b<sub>1</sub> in [#] S } is set
d is set
X is set
(x "/\") . X is set
xM is Element of the carrier of S
x "/\" xM is Element of the carrier of S
d is set
X is Element of the carrier of S
x "/\" X is Element of the carrier of S
(x "/\") . X is Element of the carrier of S
rng ((rng (x "/\")) |` (x "/\")) is Element of K10( the carrier of S)
S | (rng (x "/\")) is strict TopSpace-like T_0 T_1 T_2 SubSpace of S
[#] (S | (rng (x "/\"))) is non proper open closed dense Element of K10( the carrier of (S | (rng (x "/\"))))
the carrier of (S | (rng (x "/\"))) is set
K10( the carrier of (S | (rng (x "/\")))) is non empty cup-closed diff-closed preBoolean set
K11( the carrier of S, the carrier of (S | (rng (x "/\")))) is set
K10(K11( the carrier of S, the carrier of (S | (rng (x "/\"))))) is non empty cup-closed diff-closed preBoolean set
d is Relation-like the carrier of S -defined the carrier of (S | (rng (x "/\"))) -valued Function-like V36( the carrier of S, the carrier of (S | (rng (x "/\")))) Element of K10(K11( the carrier of S, the carrier of (S | (rng (x "/\")))))
rng d is Element of K10( the carrier of (S | (rng (x "/\"))))
S | ({x} "/\" ([#] S)) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of S
[#] (S | ({x} "/\" ([#] S))) is non empty non proper open closed dense non boundary Element of K10( the carrier of (S | ({x} "/\" ([#] S))))
the carrier of (S | ({x} "/\" ([#] S))) is non empty set
K10( the carrier of (S | ({x} "/\" ([#] S)))) is non empty cup-closed diff-closed preBoolean set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
Lim x is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is a_neighborhood of c₃
S is non empty TopSpace-like T_0 T_1 T_2 compact TopStruct
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
the carrier of x is non empty set
c₃ is Element of the carrier of x
d is Element of the carrier of x
{ (x . b₁) where b₁ is Element of the carrier of x : d <= b₁ } is set
X is set
xM is Element of the carrier of x
x . xM is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . xM is Element of the carrier of S
X is Element of K10( the carrier of S)
Cl X is closed Element of K10( the carrier of S)
bool the carrier of S is non empty cup-closed diff-closed preBoolean Element of K10(K10( the carrier of S))
K10(K10( the carrier of S)) is non empty cup-closed diff-closed preBoolean set
K11( the carrier of x,(bool the carrier of S)) is non empty set
K10(K11( the carrier of x,(bool the carrier of S))) is non empty cup-closed diff-closed preBoolean set
c₃ is non empty Relation-like the carrier of x -defined bool the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, bool the carrier of S) Element of K10(K11( the carrier of x,(bool the carrier of S)))
rng c₃ is Element of K10((bool the carrier of S))
K10((bool the carrier of S)) is non empty cup-closed diff-closed preBoolean set
dom c₃ is Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
d is Element of K10(K10( the carrier of S))
{ b₁ where b₁ is Element of the carrier of x : ex b₂, b₃ being Element of K10( the carrier of S) st
( b₂ = { (x . b₄) where b₄ is Element of the carrier of x : b₁ <= b₄ } & b₃ = Cl b₂ ) } is set
xM is set
meet xM is set
x is non empty set
the Element of x is Element of x
A is set
c₃ . A is set
M is Element of the carrier of x
c₃ . M is Element of bool the carrier of S
i2 is Element of the carrier of x
R is Element of K10( the carrier of S)
{ (x . b₁) where b₁ is Element of the carrier of x : i2 <= b₁ } is set
Cl R is closed Element of K10( the carrier of S)
j2 is non empty set
j is Element of x
c₁₅ is set
c₃ . c₁₅ is set
V is Element of the carrier of x
c₃ . V is Element of bool the carrier of S
j is Element of the carrier of x
s is Element of K10( the carrier of S)
{ (x . b₁) where b₁ is Element of the carrier of x : j <= b₁ } is set
Cl s is closed Element of K10( the carrier of S)
s9 is Element of j2
j1 is Element of j2
s1 is Element of the carrier of x
{ (x . b₁) where b₁ is Element of the carrier of x : s1 <= b₁ } is set
ss is Element of K10( the carrier of S)
Cl ss is closed Element of K10( the carrier of S)
OO is closed Element of K10( the carrier of S)
K11(x,j2) is non empty set
K10(K11(x,j2)) is non empty cup-closed diff-closed preBoolean set
j is non empty Relation-like x -defined j2 -valued Function-like V34(x) V36(x,j2) Element of K10(K11(x,j2))
rng j is Element of K10(j2)
K10(j2) is non empty cup-closed diff-closed preBoolean set
[#] x is non empty non proper lower upper Element of K10( the carrier of x)
c₁₅ is set
dom j is Element of K10(x)
K10(x) is non empty cup-closed diff-closed preBoolean set
V is set
j . V is set
s is Element of x
j . s is Element of j2
j is Element of the carrier of x
j1 is Element of K10( the carrier of S)
s9 is Element of K10( the carrier of S)
{ (x . b₁) where b₁ is Element of the carrier of x : j <= b₁ } is set
Cl s9 is closed Element of K10( the carrier of S)
K10(([#] x)) is non empty cup-closed diff-closed preBoolean set
dom j is Element of K10(x)
K10(x) is non empty cup-closed diff-closed preBoolean set
c₁₅ is Element of K10(([#] x))
V is Element of the carrier of x
x . V is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . V is Element of the carrier of S
s is set
j . s is set
j is Element of the carrier of x
j1 is Element of K10( the carrier of S)
s9 is Element of K10( the carrier of S)
{ (x . b₁) where b₁ is Element of the carrier of x : j <= b₁ } is set
Cl s9 is closed Element of K10( the carrier of S)
X is Element of K10( the carrier of S)
xM is set
c₃ . xM is set
x is Element of the carrier of x
c₃ . x is Element of bool the carrier of S
Cl X is closed Element of K10( the carrier of S)
A is Element of the carrier of x
x is Element of K10( the carrier of S)
{ (x . b₁) where b₁ is Element of the carrier of x : A <= b₁ } is set
Cl x is closed Element of K10( the carrier of S)
meet d is Element of K10( the carrier of S)
X is set
xM is Element of the carrier of S
x is a_neighborhood of xM
the carrier of S \ x is Element of K10( the carrier of S)
x is Element of the carrier of x
c₃ . x is Element of bool the carrier of S
M is Element of the carrier of x
A is Element of K10( the carrier of S)
{ (x . b₁) where b₁ is Element of the carrier of x : M <= b₁ } is set
Cl A is closed Element of K10( the carrier of S)
x /\ A is Element of K10( the carrier of S)
R is set
i2 is Element of the carrier of x
x . i2 is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . i2 is Element of the carrier of S
Int x is open Element of K10( the carrier of S)
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
c₃ is non empty transitive directed subnet of x
d is Element of the carrier of S
X is a_neighborhood of d
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
c₃ is Element of the carrier of S
the carrier of x is non empty set
the Element of the carrier of x is Element of the carrier of x
OpenNeighborhoods c₃ is non empty transitive directed RelStr
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } is strict RelStr
(InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) ~ is strict RelStr
the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) is set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } )))
K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } )) is set
K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ))) is non empty cup-closed diff-closed preBoolean set
the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) ~ is Relation-like the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) -defined the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) -valued Element of K10(K11( the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ), the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } )))
RelStr(# the carrier of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ),( the InternalRel of (InclPoset { b₁ where b₁ is Element of K10( the carrier of S) : ( c₃ in b₁ & b₁ is open ) } ) ~) #) is strict RelStr
the carrier of (OpenNeighborhoods c₃) is non empty set
{ [b₁,b₂] where b₁ is Element of the carrier of x, b₂ is Element of the carrier of (OpenNeighborhoods c₃) : x . b₁ in b₂ } is set
[#] S is non empty non proper open closed dense non boundary Element of K10( the carrier of S)
x . the Element of the carrier of x is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x . the Element of the carrier of x is Element of the carrier of S
xM is Element of the carrier of (OpenNeighborhoods c₃)
[ the Element of the carrier of x,xM] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c₃))
K11( the carrier of x, the carrier of (OpenNeighborhoods c₃)) is non empty set
{ the Element of the carrier of x,xM} is non empty set
{ the Element of the carrier of x} is non empty trivial 1 -element set
{{ the Element of the carrier of x,xM},{ the Element of the carrier of x}} is non empty set
x is non empty set
A is non empty strict RelStr
the carrier of A is non empty set
M is Element of the carrier of A
M `1 is set
the mapping of x . (M `1) is set
R is Element of the carrier of x
i2 is Element of the carrier of (OpenNeighborhoods c₃)
[R,i2] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c₃))
{R,i2} is non empty set
{R} is non empty trivial 1 -element set
{{R,i2},{R}} is non empty set
x . R is Element of the carrier of S
the mapping of x . R is Element of the carrier of S
K11( the carrier of A, the carrier of S) is non empty set
K10(K11( the carrier of A, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
M is non empty Relation-like the carrier of A -defined the carrier of S -valued Function-like V34( the carrier of A) V36( the carrier of A, the carrier of S) Element of K10(K11( the carrier of A, the carrier of S))
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of K10(K11( the carrier of A, the carrier of A))
K11( the carrier of A, the carrier of A) is non empty set
K10(K11( the carrier of A, the carrier of A)) is non empty cup-closed diff-closed preBoolean set
NetStr(# the carrier of A, the InternalRel of A,M #) is non empty strict NetStr over S
the carrier of NetStr(# the carrier of A, the InternalRel of A,M #) is non empty set
i2 is Element of the carrier of NetStr(# the carrier of A, the InternalRel of A,M #)
j2 is Element of the carrier of NetStr(# the carrier of A, the InternalRel of A,M #)
j is Element of the carrier of x
c₁₅ is Element of the carrier of (OpenNeighborhoods c₃)
[j,c₁₅] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c₃))
{j,c₁₅} is non empty set
{j} is non empty trivial 1 -element set
{{j,c₁₅},{j}} is non empty set
x . j is Element of the carrier of S
the mapping of x . j is Element of the carrier of S
V is Element of the carrier of x
s is Element of the carrier of (OpenNeighborhoods c₃)
[V,s] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c₃))
{V,s} is non empty set
{V} is non empty trivial 1 -element set
{{V,s},{V}} is non empty set
x . V is Element of the carrier of S
the mapping of x . V is Element of the carrier of S
j is Element of the carrier of x
c₁₅ /\ s is set
s9 is Element of the carrier of x
x . s9 is Element of the carrier of S
the mapping of x . s9 is Element of the carrier of S
[s9,(c₁₅ /\ s)] is V7() set
{s9,(c₁₅ /\ s)} is non empty set
{s9} is non empty trivial 1 -element set
{{s9,(c₁₅ /\ s)},{s9}} is non empty set
j1 is Element of the carrier of NetStr(# the carrier of A, the InternalRel of A,M #)
ss is Element of the carrier of A
ss `1 is set
ss `2 is set
s1 is Element of the carrier of A
s1 `1 is set
s1 `2 is set
OO is Element of the carrier of A
OO `1 is set
OO `2 is set
i2 is non empty directed NetStr over S
the carrier of i2 is non empty set
j2 is Element of the carrier of i2
j is Element of the carrier of i2
c₁₅ is Element of the carrier of i2
V is Element of the carrier of A
s is Element of the carrier of A
V `1 is set
s `1 is set
s `2 is set
V `2 is set
s9 is Element of the carrier of x
j1 is Element of the carrier of x
j is Element of the carrier of A
j `1 is set
j `2 is set
s1 is Element of the carrier of x
ss is Element of the carrier of x
j2 is non empty transitive directed NetStr over S
j is Element of the carrier of A
j `1 is set
c<sub>15</sub> is Element of the carrier of x
V is Element of the carrier of (OpenNeighborhoods c<sub>3</sub>)
[c<sub>15</sub>,V] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c<sub>3</sub>))
{c<sub>15</sub>,V} is non empty set
{c<sub>15</sub>} is non empty trivial 1 -element set
{{c<sub>15</sub>,V},{c<sub>15</sub>}} is non empty set
x . c<sub>15</sub> is Element of the carrier of S
the mapping of x . c<sub>15</sub> is Element of the carrier of S
K11( the carrier of A, the carrier of x) is non empty set
K10(K11( the carrier of A, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
j is non empty Relation-like the carrier of A -defined the carrier of x -valued Function-like V34( the carrier of A) V36( the carrier of A, the carrier of x) Element of K10(K11( the carrier of A, the carrier of x))
the carrier of j2 is non empty set
K11( the carrier of j2, the carrier of x) is non empty set
K10(K11( the carrier of j2, the carrier of x)) is non empty cup-closed diff-closed preBoolean set
c<sub>15</sub> is non empty Relation-like the carrier of j2 -defined the carrier of x -valued Function-like V34( the carrier of j2) V36( the carrier of j2, the carrier of x) Element of K10(K11( the carrier of j2, the carrier of x))
the mapping of j2 is non empty Relation-like the carrier of j2 -defined the carrier of S -valued Function-like V34( the carrier of j2) V36( the carrier of j2, the carrier of S) Element of K10(K11( the carrier of j2, the carrier of S))
K11( the carrier of j2, the carrier of S) is non empty set
K10(K11( the carrier of j2, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of x * c<sub>15</sub> is non empty Relation-like the carrier of j2 -defined the carrier of S -valued Function-like V34( the carrier of j2) V36( the carrier of j2, the carrier of S) Element of K10(K11( the carrier of j2, the carrier of S))
V is set
M . V is set
( the mapping of x * c<sub>15</sub>) . V is set
V `1 is set
the mapping of x . (V `1) is set
c<sub>15</sub> . V is set
the mapping of x . (c<sub>15</sub> . V) is set
V is Element of the carrier of x
x . V is Element of the carrier of S
the mapping of x . V is Element of the carrier of S
[V,xM] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c<sub>3</sub>))
{V,xM} is non empty set
{V} is non empty trivial 1 -element set
{{V,xM},{V}} is non empty set
s is Element of the carrier of j2
j is Element of the carrier of j2
c<sub>15</sub> . j is Element of the carrier of x
s9 is Element of the carrier of A
j1 is Element of the carrier of A
s9 `1 is set
j1 `1 is set
j1 `2 is set
s9 `2 is set
j `1 is set
s1 is Element of the carrier of x
ss is Element of the carrier of x
j is non empty transitive directed subnet of x
Lim j is Element of K10( the carrier of S)
V is a_neighborhood of c₃
Int V is open Element of K10( the carrier of S)
s is Element of the carrier of x
x . s is Element of the carrier of S
the mapping of x . s is Element of the carrier of S
[s,(Int V)] is V7() Element of K11( the carrier of x,K10( the carrier of S))
K11( the carrier of x,K10( the carrier of S)) is non empty set
{s,(Int V)} is non empty set
{s} is non empty trivial 1 -element set
{{s,(Int V)},{s}} is non empty set
the carrier of j is non empty set
j is Element of the carrier of j
s9 is Element of the carrier of j
j . s9 is Element of the carrier of S
the mapping of j is non empty Relation-like the carrier of j -defined the carrier of S -valued Function-like V34( the carrier of j) V36( the carrier of j, the carrier of S) Element of K10(K11( the carrier of j, the carrier of S))
K11( the carrier of j, the carrier of S) is non empty set
K10(K11( the carrier of j, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of j . s9 is Element of the carrier of S
j1 is Element of the carrier of A
s1 is Element of the carrier of A
j `1 is set
s9 `1 is set
s9 `2 is set
j `2 is set
ss is Element of the carrier of x
OO is Element of the carrier of (OpenNeighborhoods c₃)
[ss,OO] is V7() Element of K11( the carrier of x, the carrier of (OpenNeighborhoods c₃))
{ss,OO} is non empty set
{ss} is non empty trivial 1 -element set
{{ss,OO},{ss}} is non empty set
x . ss is Element of the carrier of S
the mapping of x . ss is Element of the carrier of S
the mapping of x . (s9 `1) is set
c₂₄ is Element of the carrier of x
c₂₅ is Element of the carrier of x
S is non empty TopSpace-like T_0 T_1 T_2 compact TopStruct
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
Lim x is trivial Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is non empty transitive directed subnet of x
X is Element of the carrier of S
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of S
c₃ is non empty transitive directed NetStr over S
the mapping of c₃ is non empty Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
the carrier of c₃ is non empty set
K11( the carrier of c₃, the carrier of S) is non empty set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of c₃ is Element of K10( the carrier of S)
d is Element of K10( the carrier of S)
X is non empty transitive directed subnet of c₃
Lim X is Element of K10( the carrier of S)
the mapping of X is non empty Relation-like the carrier of X -defined the carrier of S -valued Function-like V34( the carrier of X) V36( the carrier of X, the carrier of S) Element of K10(K11( the carrier of X, the carrier of S))
the carrier of X is non empty set
K11( the carrier of X, the carrier of S) is non empty set
K10(K11( the carrier of X, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of X is Element of K10( the carrier of S)
K11( the carrier of X, the carrier of c₃) is non empty set
K10(K11( the carrier of X, the carrier of c₃)) is non empty cup-closed diff-closed preBoolean set
xM is Element of K10( the carrier of S)
x is non empty Relation-like the carrier of X -defined the carrier of c₃ -valued Function-like V34( the carrier of X) V36( the carrier of X, the carrier of c₃) Element of K10(K11( the carrier of X, the carrier of c₃))
the mapping of c₃ * x is non empty Relation-like the carrier of X -defined the carrier of S -valued Function-like V34( the carrier of X) V36( the carrier of X, the carrier of S) Element of K10(K11( the carrier of X, the carrier of S))
Cl xM is closed Element of K10( the carrier of S)
Cl d is closed Element of K10( the carrier of S)
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of x is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is Element of the carrier of S
X is Element of the carrier of S
dom the mapping of x is Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
xM is set
the mapping of x . xM is set
x is Element of the carrier of x
x . x is Element of the carrier of S
the mapping of x . x is Element of the carrier of S
uparrow (x . x) is non empty filtered upper Element of K10( the carrier of S)
{(x . x)} is non empty trivial 1 -element Element of K10( the carrier of S)
uparrow {(x . x)} is non empty upper Element of K10( the carrier of S)
Cl (uparrow (x . x)) is closed Element of K10( the carrier of S)
x is Element of the carrier of x
A is Element of the carrier of x
x . A is Element of the carrier of S
the mapping of x . A is Element of the carrier of S
x is Element of the carrier of x
(S,x,x) is non empty transitive strict directed subnet of x
A is non empty transitive directed subnet of x
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of S -valued Function-like V34( the carrier of A) V36( the carrier of A, the carrier of S) Element of K10(K11( the carrier of A, the carrier of S))
the carrier of A is non empty set
K11( the carrier of A, the carrier of S) is non empty set
K10(K11( the carrier of A, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of A is Element of K10( the carrier of S)
M is set
dom the mapping of A is Element of K10( the carrier of A)
K10( the carrier of A) is non empty cup-closed diff-closed preBoolean set
R is set
the mapping of A . R is set
i2 is Element of the carrier of A
j2 is Element of the carrier of x
A . i2 is Element of the carrier of S
the mapping of A . i2 is Element of the carrier of S
x . j2 is Element of the carrier of S
the mapping of x . j2 is Element of the carrier of S
M is a_neighborhood of c₃
R is Element of the carrier of A
i2 is Element of the carrier of x
j2 is Element of the carrier of x
x . j2 is Element of the carrier of S
the mapping of x . j2 is Element of the carrier of S
j is Element of the carrier of A
A . j is Element of the carrier of S
the mapping of A . j is Element of the carrier of S
M is non empty transitive directed subnet of A
Lim M is trivial Element of K10( the carrier of S)
the mapping of M is non empty Relation-like the carrier of M -defined the carrier of S -valued Function-like V34( the carrier of M) V36( the carrier of M, the carrier of S) Element of K10(K11( the carrier of M, the carrier of S))
the carrier of M is non empty set
K11( the carrier of M, the carrier of S) is non empty set
K10(K11( the carrier of M, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of M is Element of K10( the carrier of S)
{ b₁ where b₁ is Element of the carrier of S : b₁ "/\" (x . x) = x . x } is set
K11( the carrier of M, the carrier of A) is non empty set
K10(K11( the carrier of M, the carrier of A)) is non empty cup-closed diff-closed preBoolean set
R is Element of K10( the carrier of S)
i2 is non empty Relation-like the carrier of M -defined the carrier of A -valued Function-like V34( the carrier of M) V36( the carrier of M, the carrier of A) Element of K10(K11( the carrier of M, the carrier of A))
the mapping of A * i2 is non empty Relation-like the carrier of M -defined the carrier of S -valued Function-like V34( the carrier of M) V36( the carrier of M, the carrier of S) Element of K10(K11( the carrier of M, the carrier of S))
Cl R is closed Element of K10( the carrier of S)
i2 is Element of the carrier of S
i2 "/\" (x . x) is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of x is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is Element of the carrier of S
X is Element of the carrier of S
dom the mapping of x is Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
xM is Element of the carrier of x
x . xM is Element of the carrier of S
the mapping of x . xM is Element of the carrier of S
X "/\" (x . xM) is Element of the carrier of S
{X} is non empty trivial 1 -element Element of K10( the carrier of S)
[#] S is non empty non proper open closed dense non boundary directed filtered lower upper Element of K10( the carrier of S)
{X} "/\" ([#] S) is non empty Element of K10( the carrier of S)
xM is set
x is set
the mapping of x . x is set
x is Element of the carrier of x
x . x is Element of the carrier of S
the mapping of x . x is Element of the carrier of S
downarrow X is non empty directed lower Element of K10( the carrier of S)
downarrow {X} is non empty lower Element of K10( the carrier of S)
{ (X "/\" b₁) where b₁ is Element of the carrier of S : b₁ in [#] S } is set
xM is Element of the carrier of S
X "/\" xM is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty transitive directed NetStr over S
sup c₃ is Element of the carrier of S
the mapping of c₃ is non empty Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
the carrier of c₃ is non empty set
K11( the carrier of c₃, the carrier of S) is non empty set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of c₃,S) is Element of the carrier of S
rng the mapping of c₃ is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
d is Element of the carrier of S
X is Element of the carrier of S
"\/" ((rng the mapping of c₃),S) is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of x is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is Element of the carrier of S
X is Element of the carrier of S
dom the mapping of x is Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
xM is set
the mapping of x . xM is set
x is Element of the carrier of x
x . x is Element of the carrier of S
the mapping of x . x is Element of the carrier of S
downarrow (x . x) is non empty directed lower Element of K10( the carrier of S)
{(x . x)} is non empty trivial 1 -element Element of K10( the carrier of S)
downarrow {(x . x)} is non empty lower Element of K10( the carrier of S)
Cl (downarrow (x . x)) is closed Element of K10( the carrier of S)
x is Element of the carrier of x
A is Element of the carrier of x
x . A is Element of the carrier of S
the mapping of x . A is Element of the carrier of S
x is Element of the carrier of x
(S,x,x) is non empty transitive strict directed subnet of x
A is non empty transitive directed subnet of x
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of S -valued Function-like V34( the carrier of A) V36( the carrier of A, the carrier of S) Element of K10(K11( the carrier of A, the carrier of S))
the carrier of A is non empty set
K11( the carrier of A, the carrier of S) is non empty set
K10(K11( the carrier of A, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of A is Element of K10( the carrier of S)
M is set
dom the mapping of A is Element of K10( the carrier of A)
K10( the carrier of A) is non empty cup-closed diff-closed preBoolean set
R is set
the mapping of A . R is set
i2 is Element of the carrier of A
j2 is Element of the carrier of x
A . i2 is Element of the carrier of S
the mapping of A . i2 is Element of the carrier of S
x . j2 is Element of the carrier of S
the mapping of x . j2 is Element of the carrier of S
M is a_neighborhood of c₃
R is Element of the carrier of A
i2 is Element of the carrier of x
j2 is Element of the carrier of x
x . j2 is Element of the carrier of S
the mapping of x . j2 is Element of the carrier of S
j is Element of the carrier of A
A . j is Element of the carrier of S
the mapping of A . j is Element of the carrier of S
M is non empty transitive directed subnet of A
Lim M is trivial Element of K10( the carrier of S)
the mapping of M is non empty Relation-like the carrier of M -defined the carrier of S -valued Function-like V34( the carrier of M) V36( the carrier of M, the carrier of S) Element of K10(K11( the carrier of M, the carrier of S))
the carrier of M is non empty set
K11( the carrier of M, the carrier of S) is non empty set
K10(K11( the carrier of M, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of M is Element of K10( the carrier of S)
{ b₁ where b₁ is Element of the carrier of S : b₁ "\/" (x . x) = x . x } is set
K11( the carrier of M, the carrier of A) is non empty set
K10(K11( the carrier of M, the carrier of A)) is non empty cup-closed diff-closed preBoolean set
R is Element of K10( the carrier of S)
i2 is non empty Relation-like the carrier of M -defined the carrier of A -valued Function-like V34( the carrier of M) V36( the carrier of M, the carrier of A) Element of K10(K11( the carrier of M, the carrier of A))
the mapping of A * i2 is non empty Relation-like the carrier of M -defined the carrier of S -valued Function-like V34( the carrier of M) V36( the carrier of M, the carrier of S) Element of K10(K11( the carrier of M, the carrier of S))
Cl R is closed Element of K10( the carrier of S)
i2 is Element of the carrier of S
i2 "\/" (x . x) is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of x is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is Element of the carrier of S
X is Element of the carrier of S
dom the mapping of x is Element of K10( the carrier of x)
K10( the carrier of x) is non empty cup-closed diff-closed preBoolean set
xM is Element of the carrier of x
x . xM is Element of the carrier of S
the mapping of x . xM is Element of the carrier of S
X "\/" (x . xM) is Element of the carrier of S
{X} is non empty trivial 1 -element Element of K10( the carrier of S)
[#] S is non empty non proper open closed dense non boundary directed filtered lower upper Element of K10( the carrier of S)
{X} "\/" ([#] S) is non empty Element of K10( the carrier of S)
xM is set
x is set
the mapping of x . x is set
x is Element of the carrier of x
x . x is Element of the carrier of S
the mapping of x . x is Element of the carrier of S
uparrow X is non empty filtered upper Element of K10( the carrier of S)
uparrow {X} is non empty upper Element of K10( the carrier of S)
{ (X "\/" b₁) where b₁ is Element of the carrier of S : b₁ in [#] S } is set
xM is Element of the carrier of S
X "\/" xM is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is Element of the carrier of S
c₃ is non empty transitive directed NetStr over S
(S,c₃) is Element of the carrier of S
the mapping of c₃ is non empty Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
the carrier of c₃ is non empty set
K11( the carrier of c₃, the carrier of S) is non empty set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
//\ ( the mapping of c₃,S) is Element of the carrier of S
rng the mapping of c₃ is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
d is Element of the carrier of S
X is Element of the carrier of S
"/\" ((rng the mapping of c₃),S) is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima ()
the carrier of S is non empty set
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
x is non empty directed Element of K10( the carrier of S)
K11(x, the carrier of S) is non empty set
K10(K11(x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id x is non empty Relation-like x -defined x -valued Function-like one-to-one V34(x) V36(x,x) Element of K10(K11(x,x))
K11(x,x) is non empty set
K10(K11(x,x)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of S |_2 x is Relation-like x -defined x -valued Element of K10(K11(x,x))
the InternalRel of S /\ K11(x,x) is set
c₃ is non empty Relation-like x -defined the carrier of S -valued Function-like V34(x) V36(x, the carrier of S) Element of K10(K11(x, the carrier of S))
NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty transitive strict directed NetStr over S
the mapping of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty Relation-like the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) -defined the carrier of S -valued Function-like V34( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #)) V36( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of S) Element of K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of S))
the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is non empty set
K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of S) is non empty set
K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c₃ #), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
rng the mapping of NetStr(# x,( the InternalRel of S |_2 x),c₃ #) is Element of K10( the carrier of S)
x is Element of the carrier of S
{x} is non empty trivial 1 -element Element of K10( the carrier of S)
c₃ is non empty transitive directed NetStr over S
sup c₃ is Element of the carrier of S
the mapping of c₃ is non empty Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
the carrier of c₃ is non empty set
K11( the carrier of c₃, the carrier of S) is non empty set
K10(K11( the carrier of c₃, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of c₃,S) is Element of the carrier of S
x "/\" (sup c₃) is Element of the carrier of S
netmap (c₃,S) is non empty Relation-like the carrier of c₃ -defined the carrier of S -valued Function-like V34( the carrier of c₃) V36( the carrier of c₃, the carrier of S) Element of K10(K11( the carrier of c₃, the carrier of S))
rng (netmap (c₃,S)) is Element of K10( the carrier of S)
{x} "/\" (rng (netmap (c₃,S))) is Element of K10( the carrier of S)
"\/" (({x} "/\" (rng (netmap (c₃,S)))),S) is Element of the carrier of S
Lim c₃ is trivial Element of K10( the carrier of S)
x "/\" c₃ is non empty transitive strict directed NetStr over S
sup (x "/\" c₃) is Element of the carrier of S
the mapping of (x "/\" c₃) is non empty Relation-like the carrier of (x "/\" c₃) -defined the carrier of S -valued Function-like V34( the carrier of (x "/\" c₃)) V36( the carrier of (x "/\" c₃), the carrier of S) Element of K10(K11( the carrier of (x "/\" c₃), the carrier of S))
the carrier of (x "/\" c₃) is non empty set
K11( the carrier of (x "/\" c₃), the carrier of S) is non empty set
K10(K11( the carrier of (x "/\" c₃), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of (x "/\" c₃),S) is Element of the carrier of S
Lim (x "/\" c₃) is trivial Element of K10( the carrier of S)
x "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
d is non empty transitive directed convergent NetStr over S
lim d is Element of the carrier of S
x "/\" (lim d) is Element of the carrier of S
x "/\" d is non empty transitive strict directed NetStr over S
Lim (x "/\" d) is trivial Element of K10( the carrier of S)
xM is non empty transitive directed convergent NetStr over S
lim xM is Element of the carrier of S
the mapping of xM is non empty Relation-like the carrier of xM -defined the carrier of S -valued Function-like V34( the carrier of xM) V36( the carrier of xM, the carrier of S) Element of K10(K11( the carrier of xM, the carrier of S))
the carrier of xM is non empty set
K11( the carrier of xM, the carrier of S) is non empty set
K10(K11( the carrier of xM, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of xM,S) is Element of the carrier of S
rng the mapping of xM is Element of K10( the carrier of S)
"\/" ((rng the mapping of xM),S) is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
sup x is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of x,S) is Element of the carrier of S
Lim x is trivial Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is Element of the carrier of S
c₃ is Element of the carrier of S
rng the mapping of x is Element of K10( the carrier of S)
d is Element of the carrier of S
xM is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
(S,x) is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
//\ ( the mapping of x,S) is Element of the carrier of S
Lim x is trivial Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
c₃ is Element of the carrier of S
d is Element of the carrier of S
c₃ is Element of the carrier of S
rng the mapping of x is Element of K10( the carrier of S)
d is Element of the carrier of S
xM is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
(S) is non empty reflexive transitive antisymmetric strict directed antitone eventually-filtered NetStr over S
(S,(S)) is Element of the carrier of S
the mapping of (S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
the carrier of (S) is non empty set
K11( the carrier of (S), the carrier of S) is non empty set
K10(K11( the carrier of (S), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
//\ ( the mapping of (S),S) is Element of the carrier of S
x is Element of the carrier of S
rng the mapping of (S) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) monotone Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
rng (id S) is Element of K10( the carrier of S)
"/\" ( the carrier of S,S) is Element of the carrier of S
(S) is non empty reflexive transitive antisymmetric strict directed monotone eventually-directed NetStr over S
sup (S) is Element of the carrier of S
the mapping of (S) is non empty Relation-like the carrier of (S) -defined the carrier of S -valued Function-like V34( the carrier of (S)) V36( the carrier of (S), the carrier of S) Element of K10(K11( the carrier of (S), the carrier of S))
the carrier of (S) is non empty set
K11( the carrier of (S), the carrier of S) is non empty set
K10(K11( the carrier of (S), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of (S),S) is Element of the carrier of S
x is Element of the carrier of S
rng the mapping of (S) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V34( the carrier of S) V36( the carrier of S, the carrier of S) monotone Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty set
K10(K11( the carrier of S, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V34( the carrier of S) V36( the carrier of S, the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
rng (id S) is Element of K10( the carrier of S)
"\/" ( the carrier of S,S) is Element of the carrier of S
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric with_suprema with_infima compact ()
the carrier of S is non empty set
x is non empty transitive directed NetStr over S
sup x is Element of the carrier of S
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))
the carrier of x is non empty set
K11( the carrier of x, the carrier of S) is non empty set
K10(K11( the carrier of x, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of x,S) is Element of the carrier of S
Lim x is trivial Element of K10( the carrier of S)
K10( the carrier of S) is non empty cup-closed diff-closed preBoolean set