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