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

d is Element of the carrier of S

X is Element of the carrier of S

c

c

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

x is Element of the carrier of x

c

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

the carrier of c

d is non empty RelStr

the carrier of d is non empty set

K11( the carrier of c

K10(K11( the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

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

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

the carrier of c

d is non empty RelStr

the carrier of d is non empty set

K11( the carrier of c

K10(K11( the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

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

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

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

c

d is Element of the carrier of S

d "/\" x is Element of the carrier of S

c

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

c

d is Element of the carrier of S

x "\/" d is Element of the carrier of S

c

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

c

d is Element of the carrier of S

d "\/" x is Element of the carrier of S

c

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

c

d is Element of the carrier of S

x "/\" d is Element of the carrier of S

c

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

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

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

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

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

NetStr(# x,( the InternalRel of S |_2 x),c

the carrier of NetStr(# x,( the InternalRel of S |_2 x),c

the InternalRel of NetStr(# x,( the InternalRel of S |_2 x),c

K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c

K10(K11( the carrier of NetStr(# x,( the InternalRel of S |_2 x),c

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

NetStr(# x,( the InternalRel of S |_2 x),c

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

NetStr(# x,( the InternalRel of S |_2 x),c

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

"\/" (c

x "/\" ("\/" (c

{x} "/\" c

"\/" (({x} "/\" c

K11(c

K10(K11(c

id c

K11(c

K10(K11(c

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

the InternalRel of S /\ K11(c

d is non empty Relation-like c

NetStr(# c

netmap (NetStr(# c

the carrier of NetStr(# c

K11( the carrier of NetStr(# c

K10(K11( the carrier of NetStr(# c

the mapping of NetStr(# c

\\/ ((netmap (NetStr(# c

sup NetStr(# c

\\/ ( the mapping of NetStr(# c

d .: c

rng (netmap (NetStr(# c

x "/\" (\\/ ((netmap (NetStr(# c

S is non empty RelStr

the carrier of S is non empty set

x is Element of the carrier of S

c

x "/\" c

the carrier of (x "/\" c

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

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

the InternalRel of (x "/\" c

K11( the carrier of (x "/\" c

K10(K11( the carrier of (x "/\" c

RelStr(# the carrier of (x "/\" c

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

x "/\" c

S is non empty RelStr

the carrier of S is non empty set

x is Element of the carrier of S

c

x "/\" c

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

the carrier of (x "/\" c

the InternalRel of (x "/\" c

K11( the carrier of (x "/\" c

K10(K11( the carrier of (x "/\" c

RelStr(# the carrier of (x "/\" c

S is non empty RelStr

the carrier of S is non empty set

x is Element of the carrier of S

c

x "/\" c

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

the carrier of (x "/\" c

the InternalRel of (x "/\" c

K11( the carrier of (x "/\" c

K10(K11( the carrier of (x "/\" c

RelStr(# the carrier of (x "/\" c

S is non empty RelStr

the carrier of S is non empty set

x is Element of the carrier of S

c

x "/\" c

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

the carrier of (x "/\" c

the InternalRel of (x "/\" c

K11( the carrier of (x "/\" c

K10(K11( the carrier of (x "/\" c

RelStr(# the carrier of (x "/\" c

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

FinSups c

the carrier of (FinSups c

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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

the mapping of c

K11( the carrier of c

K10(K11( the carrier of c

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

(S) . c

the mapping of (S) . c

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

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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

the mapping of c

K11( the carrier of c

K10(K11( the carrier of c

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

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

(S) . c

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

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

{c

{c

{{c

[X,c

{X,c

{X} is non empty trivial 1 -element set

{{X,c

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

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

(S,x,c

the carrier of (S,x,c

{ b

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

(S,x,c

the carrier of (S,x,c

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

(S,x,c

the mapping of (S,x,c

the carrier of (S,x,c

the carrier of S is non empty set

K11( the carrier of (S,x,c

K10(K11( the carrier of (S,x,c

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V34( the carrier of x) V36( the carrier of x, the carrier of S) Element of K10(K11( the carrier of x, the carrier of S))

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

the InternalRel of (S,x,c

K11( the carrier of (S,x,c

K10(K11( the carrier of (S,x,c

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

the InternalRel of x /\ K11( the carrier of (S,x,c

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

(S,x,c

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

(S,x,c

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

(S,x,c

the carrier of (S,x,c

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

(S,x,c

the carrier of (S,x,c

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

(S,x,c

the carrier of (S,x,c

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

(S,x,c

the carrier of (S,x,c

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

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

(S,x,c

the carrier of (S,x,c

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

the mapping of (S,x,c

K11( the carrier of (S,x,c

K10(K11( the carrier of (S,x,c

the mapping of (S,x,c

the mapping of x | the carrier of (S,x,c

( the mapping of x | the carrier of (S,x,c

S is non empty 1-sorted

x is non empty directed NetStr over S

the carrier of x is non empty set

c

(S,x,c

the carrier of (S,x,c

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

the mapping of (S,x,c

K11( the carrier of (S,x,c

K10(K11( the carrier of (S,x,c

the mapping of (S,x,c

the mapping of x | the carrier of (S,x,c

( the mapping of x | the carrier of (S,x,c

S is non empty 1-sorted

x is non empty transitive directed NetStr over S

the carrier of x is non empty set

c

(S,x,c

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