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

{{},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
c3 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
c3 . X is Element of the carrier of x
c3 . 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
c3 . d is Element of the carrier of x
x is Element of the carrier of x
c3 . 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
c3 is non empty RelStr
the carrier of c3 is non empty set
d is non empty RelStr
the carrier of d is non empty set
K11( the carrier of c3, the carrier of d) is non empty set
K10(K11( the carrier of c3, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is non empty set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) 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 c3 -defined the carrier of d -valued Function-like V34( the carrier of c3) V36( the carrier of c3, the carrier of d) Element of K10(K11( the carrier of c3, the carrier of d))
A is Element of the carrier of c3
M is Element of the carrier of c3
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
c3 is non empty RelStr
the carrier of c3 is non empty set
d is non empty RelStr
the carrier of d is non empty set
K11( the carrier of c3, the carrier of d) is non empty set
K10(K11( the carrier of c3, the carrier of d)) is non empty cup-closed diff-closed preBoolean set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is non empty set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) 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 c3 -defined the carrier of d -valued Function-like V34( the carrier of c3) V36( the carrier of c3, the carrier of d) Element of K10(K11( the carrier of c3, the carrier of d))
A is Element of the carrier of c3
M is Element of the carrier of c3
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
c3 is Element of K10(K10( the carrier of S))
d is Element of K10(K10( the carrier of x))

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)
{ b1 where b1 is Element of the carrier of S : b1 "/\" x = x } is set
c3 is set
d is Element of the carrier of S
d "/\" x is Element of the carrier of S
c3 is set
d is Element of the carrier of S
d "/\" x is Element of the carrier of S

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 "\/" b1) where b1 is Element of the carrier of S : b1 in [#] S } is set
c3 is set
d is Element of the carrier of S
x "\/" d is Element of the carrier of S
c3 is set
d is Element of the carrier of S
x "\/" d is Element of the carrier of S

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)
{ b1 where b1 is Element of the carrier of S : b1 "\/" x = x } is set
c3 is set
d is Element of the carrier of S
d "\/" x is Element of the carrier of S
c3 is set
d is Element of the carrier of S
d "\/" x is Element of the carrier of S

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 "/\" b1) where b1 is Element of the carrier of S : b1 in [#] S } is set
c3 is set
d is Element of the carrier of S
x "/\" d is Element of the carrier of S
c3 is set
d is Element of the carrier of S
x "/\" d is Element of the carrier of S

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 "/\") .: () is non empty Element of K10( the carrier of S)
c3 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
c3 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

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)
c3 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
c3 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
c3 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),c3 #) is non empty strict NetStr over S
the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #) is non empty set
the InternalRel of NetStr(# x,( the InternalRel of S |_2 x),c3 #) is Relation-like the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #) -defined the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #) -valued Element of K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #), the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #)))
K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #), the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #)) is non empty set
K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #), the carrier of NetStr(# x,( the InternalRel of S |_2 x),c3 #))) is non empty cup-closed diff-closed preBoolean set
X is 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
c3 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),c3 #) 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
c3 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),c3 #) 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)
c3 is non empty directed Element of K10( the carrier of S)
"\/" (c3,S) is Element of the carrier of S
x "/\" ("\/" (c3,S)) is Element of the carrier of S
{x} "/\" c3 is non empty Element of K10( the carrier of S)
"\/" (({x} "/\" c3),S) is Element of the carrier of S
K11(c3, the carrier of S) is non empty set
K10(K11(c3, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
id c3 is non empty Relation-like c3 -defined c3 -valued Function-like one-to-one V34(c3) V36(c3,c3) Element of K10(K11(c3,c3))
K11(c3,c3) is non empty set
K10(K11(c3,c3)) 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 c3 is Relation-like c3 -defined c3 -valued Element of K10(K11(c3,c3))
the InternalRel of S /\ K11(c3,c3) is set
d is non empty Relation-like c3 -defined the carrier of S -valued Function-like V34(c3) V36(c3, the carrier of S) Element of K10(K11(c3, the carrier of S))
NetStr(# c3,( the InternalRel of S |_2 c3),d #) is non empty transitive strict directed NetStr over S
netmap (NetStr(# c3,( the InternalRel of S |_2 c3),d #),S) is non empty Relation-like the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #) -defined the carrier of S -valued Function-like V34( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #)) V36( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #), the carrier of S) Element of K10(K11( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #), the carrier of S))
the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #) is non empty set
K11( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #), the carrier of S) is non empty set
K10(K11( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of NetStr(# c3,( the InternalRel of S |_2 c3),d #) is non empty Relation-like the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #) -defined the carrier of S -valued Function-like V34( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #)) V36( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #), the carrier of S) Element of K10(K11( the carrier of NetStr(# c3,( the InternalRel of S |_2 c3),d #), the carrier of S))
\\/ ((netmap (NetStr(# c3,( the InternalRel of S |_2 c3),d #),S)),S) is Element of the carrier of S
sup NetStr(# c3,( the InternalRel of S |_2 c3),d #) is Element of the carrier of S
\\/ ( the mapping of NetStr(# c3,( the InternalRel of S |_2 c3),d #),S) is Element of the carrier of S
d .: c3 is Element of K10( the carrier of S)
rng (netmap (NetStr(# c3,( the InternalRel of S |_2 c3),d #),S)) is Element of K10( the carrier of S)
x "/\" (\\/ ((netmap (NetStr(# c3,( the InternalRel of S |_2 c3),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
c3 is non empty transitive directed NetStr over S
x "/\" c3 is non empty strict directed NetStr over S
the carrier of (x "/\" c3) is non empty set
X is Element of the carrier of (x "/\" c3)
xM is Element of the carrier of (x "/\" c3)
x is Element of the carrier of (x "/\" c3)
the carrier of c3 is non empty set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is non empty set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) is strict RelStr
the InternalRel of (x "/\" c3) is Relation-like the carrier of (x "/\" c3) -defined the carrier of (x "/\" c3) -valued Element of K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)))
K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)) is non empty set
K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c3), the InternalRel of (x "/\" c3) #) is strict RelStr
x is Element of the carrier of c3
A is Element of the carrier of c3
M is Element of the carrier of c3
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c3 is non empty transitive directed NetStr over S
x "/\" c3 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
c3 is non empty reflexive NetStr over S
x "/\" c3 is non empty strict NetStr over S
the carrier of c3 is non empty set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is non empty set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) is strict RelStr
the carrier of (x "/\" c3) is non empty set
the InternalRel of (x "/\" c3) is Relation-like the carrier of (x "/\" c3) -defined the carrier of (x "/\" c3) -valued Element of K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)))
K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)) is non empty set
K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c3), the InternalRel of (x "/\" c3) #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c3 is non empty antisymmetric NetStr over S
x "/\" c3 is non empty strict NetStr over S
the carrier of c3 is non empty set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is non empty set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) is strict RelStr
the carrier of (x "/\" c3) is non empty set
the InternalRel of (x "/\" c3) is Relation-like the carrier of (x "/\" c3) -defined the carrier of (x "/\" c3) -valued Element of K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)))
K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)) is non empty set
K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c3), the InternalRel of (x "/\" c3) #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
c3 is non empty transitive NetStr over S
x "/\" c3 is non empty strict NetStr over S
the carrier of c3 is non empty set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is non empty set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) is strict RelStr
the carrier of (x "/\" c3) is non empty set
the InternalRel of (x "/\" c3) is Relation-like the carrier of (x "/\" c3) -defined the carrier of (x "/\" c3) -valued Element of K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)))
K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3)) is non empty set
K10(K11( the carrier of (x "/\" c3), the carrier of (x "/\" c3))) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of (x "/\" c3), the InternalRel of (x "/\" c3) #) 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
c3 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 c3 is non empty directed NetStr over S
the carrier of (FinSups c3) is non empty set
d is Element of the carrier of (FinSups c3)
X is Element of the carrier of (FinSups c3)
xM is Element of the carrier of (FinSups c3)

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
c3 is strict NetStr over S
the carrier of c3 is set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of c3, the InternalRel of c3 #) is strict RelStr
the mapping of c3 is Relation-like the carrier of c3 -defined the carrier of S -valued Function-like V36( the carrier of c3, the carrier of S) Element of K10(K11( the carrier of c3, the carrier of S))
K11( the carrier of c3, the carrier of S) is set
K10(K11( the carrier of c3, 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 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 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 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 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
c3 is Element of the carrier of (S)
(S) . c3 is Element of the carrier of S
the mapping of (S) . c3 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) . c3 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
c3 is strict NetStr over S
the carrier of c3 is set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of K10(K11( the carrier of c3, the carrier of c3))
K11( the carrier of c3, the carrier of c3) is set
K10(K11( the carrier of c3, the carrier of c3)) is non empty cup-closed diff-closed preBoolean set
the mapping of c3 is Relation-like the carrier of c3 -defined the carrier of S -valued Function-like V36( the carrier of c3, the carrier of S) Element of K10(K11( the carrier of c3, the carrier of S))
K11( the carrier of c3, the carrier of S) is set
K10(K11( the carrier of c3, the carrier of S)) is non empty cup-closed diff-closed preBoolean set
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))
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 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 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 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
c3 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
c3 is Element of the carrier of (S)
(S) . c3 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) . c3 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
[c3,X] is V7() Element of K11( the carrier of (S), the carrier of (S))
{c3,X} is non empty set
{c3} is non empty trivial 1 -element set
{{c3,X},{c3}} is non empty set
[X,c3] is V7() Element of K11( the carrier of (S), the carrier of (S))
{X,c3} is non empty set
{X} is non empty trivial 1 -element set
{{X,c3},{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
c3 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
c3 is Element of the carrier of x
(S,x,c3) is strict NetStr over S
the carrier of (S,x,c3) is set
{ b1 where b1 is Element of the carrier of x : c3 <= b1 } 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
c3 is Element of the carrier of x
(S,x,c3) is strict NetStr over S
the carrier of (S,x,c3) 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
c3 is Element of the carrier of x
(S,x,c3) is strict NetStr over S
the mapping of (S,x,c3) is Relation-like the carrier of (S,x,c3) -defined the carrier of S -valued Function-like V34( the carrier of (S,x,c3)) V36( the carrier of (S,x,c3), the carrier of S) Element of K10(K11( the carrier of (S,x,c3), the carrier of S))
the carrier of (S,x,c3) is set
the carrier of S is non empty set
K11( the carrier of (S,x,c3), the carrier of S) is set
K10(K11( the carrier of (S,x,c3), 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,c3) 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,c3) is Relation-like the carrier of (S,x,c3) -defined the carrier of (S,x,c3) -valued Element of K10(K11( the carrier of (S,x,c3), the carrier of (S,x,c3)))
K11( the carrier of (S,x,c3), the carrier of (S,x,c3)) is set
K10(K11( the carrier of (S,x,c3), the carrier of (S,x,c3))) 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,c3) is Relation-like the carrier of (S,x,c3) -defined the carrier of (S,x,c3) -valued Element of K10(K11( the carrier of (S,x,c3), the carrier of (S,x,c3)))
the InternalRel of x /\ K11( the carrier of (S,x,c3), the carrier of (S,x,c3)) 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
c3 is Element of the carrier of x
(S,x,c3) 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
c3 is Element of the carrier of x
(S,x,c3) 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
c3 is Element of the carrier of x
(S,x,c3) is non empty reflexive strict NetStr over S
the carrier of (S,x,c3) is non empty set
d is Element of the carrier of (S,x,c3)
X is Element of the carrier of (S,x,c3)
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
c3 is Element of the carrier of x
(S,x,c3) is non empty strict NetStr over S
the carrier of (S,x,c3) is non empty set
d is Element of the carrier of (S,x,c3)
X is Element of the carrier of (S,x,c3)
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
c3 is Element of the carrier of x
(S,x,c3) is non empty reflexive strict NetStr over S
the carrier of (S,x,c3) is non empty set
d is Element of the carrier of (S,x,c3)
X is Element of the carrier of (S,x,c3)
xM is Element of the carrier of (S,x,c3)
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
c3 is Element of the carrier of x
(S,x,c3) is non empty strict NetStr over S
the carrier of (S,x,c3) is non empty set
d is Element of the carrier of (S,x,c3)
X is Element of the carrier of (S,x,c3)
xM is Element of the carrier of (S,x,c3)
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,c3) is non empty set
d is Element of the carrier of (S,x,c3)
X is Element of the carrier of (S,x,c3)
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,c3)
S is non empty 1-sorted
x is non empty reflexive NetStr over S
the carrier of x is non empty set
c3 is Element of the carrier of x
(S,x,c3) is non empty reflexive strict NetStr over S
the carrier of (S,x,c3) 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,c3)
(S,x,c3) . X is Element of the carrier of S
the mapping of (S,x,c3) is non empty Relation-like the carrier of (S,x,c3) -defined the carrier of S -valued Function-like V34( the carrier of (S,x,c3)) V36( the carrier of (S,x,c3), the carrier of S) Element of K10(K11( the carrier of (S,x,c3), the carrier of S))
K11( the carrier of (S,x,c3), the carrier of S) is non empty set
K10(K11( the carrier of (S,x,c3), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S,x,c3) . X is Element of the carrier of S
the mapping of x | the carrier of (S,x,c3) 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,c3)) . 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
c3 is Element of the carrier of x
(S,x,c3) is non empty strict NetStr over S
the carrier of (S,x,c3) 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,c3)
(S,x,c3) . X is Element of the carrier of S
the mapping of (S,x,c3) is non empty Relation-like the carrier of (S,x,c3) -defined the carrier of S -valued Function-like V34( the carrier of (S,x,c3)) V36( the carrier of (S,x,c3), the carrier of S) Element of K10(K11( the carrier of (S,x,c3), the carrier of S))
K11( the carrier of (S,x,c3), the carrier of S) is non empty set
K10(K11( the carrier of (S,x,c3), the carrier of S)) is non empty cup-closed diff-closed preBoolean set
the mapping of (S,x,c3) . X is Element of the carrier of S
the mapping of x | the carrier of (S,x,c3) 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,c3)) . 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
c3 is Element of the carrier of x
(S,x,c3) 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