:: WAYBEL_2 semantic presentation

K173() is set

K177() is non empty non trivial V39() V40() V41() non finite V51() V52() Element of bool K173()

bool K173() is non empty cup-closed diff-closed preBoolean set

K125() is non empty non trivial V39() V40() V41() non finite V51() V52() set

bool K125() is non empty non trivial cup-closed diff-closed preBoolean non finite set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V39() V40() V41() V43() V44() V45() finite finite-yielding V50() V51() V53( {} ) set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V39() V40() V41() V43() V44() V45() finite finite-yielding V50() V51() V53( {} ) set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V39() V40() V41() V43() V44() V45() finite finite-yielding V50() V51() V53( {} ) set

1 is non empty V39() V40() V41() V45() finite V51() Element of K177()

{{},1} is non empty finite V50() set

bool K177() is non empty non trivial cup-closed diff-closed preBoolean non finite set

H is non empty set

a is non empty set

[:H,a:] is non empty Relation-like set

bool [:H,a:] is non empty cup-closed diff-closed preBoolean set

bool H is non empty cup-closed diff-closed preBoolean set

X is non empty Relation-like H -defined a -valued Function-like V31(H) V33(H,a) Element of bool [:H,a:]

X1 is non empty Element of bool H

X .: X1 is Element of bool a

bool a is non empty cup-closed diff-closed preBoolean set

the Element of X1 is Element of X1

dom X is non empty Element of bool H

H is non empty RelStr

the carrier of H is non empty set

a is Element of the carrier of H

X is Element of the carrier of H

X1 is Element of the carrier of H

xx is Element of the carrier of H

X1 is Element of the carrier of H

xx is Element of the carrier of H

the carrier of H is non empty set

a is Element of the carrier of H

X is Element of the carrier of H

X1 is Element of the carrier of H

xx is Element of the carrier of H

X1 is Element of the carrier of H

xx is Element of the carrier of H

H is non empty V70() reflexive transitive antisymmetric connected non void with_suprema with_infima RelStr

[#] H is non empty non proper directed filtered lower upper Element of bool the carrier of H

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of H

X is Element of the carrier of H

{X} is non empty trivial finite V53(1) Element of bool the carrier of H

{X} "/\" a is non empty Element of bool the carrier of H

X1 is non empty directed Element of bool the carrier of H

X1 "/\" a is non empty directed Element of bool the carrier of H

H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of H

X is Element of the carrier of H

{X} is non empty trivial finite V53(1) Element of bool the carrier of H

{X} "\/" a is non empty Element of bool the carrier of H

X1 is non empty directed Element of bool the carrier of H

X1 "\/" a is non empty directed Element of bool the carrier of H

H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of H

X is non empty directed Element of bool the carrier of H

a "\/" X is non empty directed Element of bool the carrier of H

"\/" ((a "\/" X),H) is Element of the carrier of H

{ (b

the Element of X is Element of X

xx is Element of the carrier of H

xx "\/" the Element of X is Element of the carrier of H

f is Element of the carrier of H

H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of H

X is non empty directed Element of bool the carrier of H

a "\/" X is non empty directed Element of bool the carrier of H

"\/" ((a "\/" X),H) is Element of the carrier of H

"\/" (a,H) is Element of the carrier of H

"\/" (X,H) is Element of the carrier of H

("\/" (a,H)) "\/" ("\/" (X,H)) is Element of the carrier of H

("\/" ((a "\/" X),H)) "\/" ("\/" ((a "\/" X),H)) is Element of the carrier of H

H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr

[:H,H:] is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

proj2 a is Element of bool the carrier of H

proj1 a is Element of bool the carrier of H

{ ("\/" (({b

{ ("\/" (b

( b

{ ("\/" (b

xx is set

X1 is non empty directed Element of bool the carrier of H

X is non empty directed Element of bool the carrier of H

f is Element of the carrier of H

{f} is non empty trivial finite V53(1) Element of bool the carrier of H

{f} "/\" X1 is non empty Element of bool the carrier of H

"\/" (({f} "/\" X1),H) is Element of the carrier of H

h is non empty directed Element of bool the carrier of H

h "/\" X1 is non empty directed Element of bool the carrier of H

xx is set

f is non empty directed Element of bool the carrier of H

"\/" (f,H) is Element of the carrier of H

h is Element of the carrier of H

{h} is non empty trivial finite V53(1) Element of bool the carrier of H

{h} "/\" (proj2 a) is Element of bool the carrier of H

H is non empty V70() reflexive transitive antisymmetric non void with_infima RelStr

[:H,H:] is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

proj2 a is Element of bool the carrier of H

proj1 a is Element of bool the carrier of H

{ b

( b

union { b

( b

(proj1 a) "/\" (proj2 a) is Element of bool the carrier of H

{ (b

{ b

union { b

f is set

h is set

a is non empty directed Element of bool the carrier of H

y is Element of the carrier of H

{y} is non empty trivial finite V53(1) Element of bool the carrier of H

{y} "/\" (proj2 a) is Element of bool the carrier of H

y is Element of the carrier of H

{y} is non empty trivial finite V53(1) Element of bool the carrier of H

{y} "/\" (proj2 a) is Element of bool the carrier of H

{ (y "/\" b

Y is Element of the carrier of H

y "/\" Y is Element of the carrier of H

f is set

h is Element of the carrier of H

a is Element of the carrier of H

h "/\" a is Element of the carrier of H

{h} is non empty trivial finite V53(1) Element of bool the carrier of H

y is non empty directed Element of bool the carrier of H

xx is non empty directed Element of bool the carrier of H

y "/\" xx is non empty directed Element of bool the carrier of H

{h} "/\" (proj2 a) is Element of bool the carrier of H

{ (h "/\" b

H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr

[:H,H:] is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

proj2 a is Element of bool the carrier of H

proj1 a is Element of bool the carrier of H

{ b

( b

union { b

( b

X1 is non empty directed Element of bool the carrier of H

X is non empty directed Element of bool the carrier of H

{ b

( b

union { b

( b

f is set

h is set

a is non empty directed Element of bool the carrier of H

y is Element of the carrier of H

{y} is non empty trivial finite V53(1) Element of bool the carrier of H

{y} "/\" X1 is non empty Element of bool the carrier of H

f is Element of bool the carrier of H

X "/\" X1 is non empty directed Element of bool the carrier of H

H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr

[:H,H:] is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

proj2 a is Element of bool the carrier of H

proj1 a is Element of bool the carrier of H

{ ("\/" (b

( b

X1 is non empty directed Element of bool the carrier of H

X is non empty directed Element of bool the carrier of H

{ ("\/" (b

f is set

h is non empty directed Element of bool the carrier of H

"\/" (h,H) is Element of the carrier of H

a is Element of the carrier of H

{a} is non empty trivial finite V53(1) Element of bool the carrier of H

{a} "/\" X1 is non empty Element of bool the carrier of H

{ b

union { b

a is set

y is set

Y is non empty directed Element of bool the carrier of H

z is Element of the carrier of H

{z} is non empty trivial finite V53(1) Element of bool the carrier of H

{z} "/\" X1 is non empty Element of bool the carrier of H

a is Element of bool the carrier of H

"\/" (a,H) is Element of the carrier of H

f is Element of bool the carrier of H

Y is Element of the carrier of H

z is Element of the carrier of H

y is set

z1 is non empty directed Element of bool the carrier of H

x is Element of the carrier of H

{x} is non empty trivial finite V53(1) Element of bool the carrier of H

{x} "/\" X1 is non empty Element of bool the carrier of H

x is Element of the carrier of H

{x} is non empty trivial finite V53(1) Element of bool the carrier of H

{x} "/\" X1 is non empty Element of bool the carrier of H

{ (x "/\" b

"\/" (z1,H) is Element of the carrier of H

d2 is Element of the carrier of H

{d2} is non empty trivial finite V53(1) Element of bool the carrier of H

{d2} "/\" X1 is non empty Element of bool the carrier of H

d2 is Element of the carrier of H

x "/\" d2 is Element of the carrier of H

Y is Element of the carrier of H

z is non empty directed Element of bool the carrier of H

"\/" (z,H) is Element of the carrier of H

y is Element of the carrier of H

{y} is non empty trivial finite V53(1) Element of bool the carrier of H

{y} "/\" X1 is non empty Element of bool the carrier of H

H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr

[:H,H:] is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

proj2 a is Element of bool the carrier of H

proj1 a is Element of bool the carrier of H

{ ("\/" (b

( b

"\/" ( { ("\/" (b

( b

{ b

( b

union { b

( b

"\/" ((union { b

( b

{ ("\/" (b

{ b

union { b

"\/" ((union { b

X is Element of the carrier of H

X1 is non empty directed Element of bool the carrier of H

"\/" (X1,H) is Element of the carrier of H

xx is Element of the carrier of H

{xx} is non empty trivial finite V53(1) Element of bool the carrier of H

{xx} "/\" (proj2 a) is Element of bool the carrier of H

H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr

[:H,H:] is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

proj2 a is Element of bool the carrier of H

proj1 a is Element of bool the carrier of H

{ ("\/" (b

( b

"\/" ( { ("\/" (b

( b

{ b

( b

union { b

( b

"\/" ((union { b

( b

{ ("\/" (b

"\/" ( { ("\/" (b

{ b

union { b

"\/" ((union { b

X is Element of the carrier of H

X1 is set

xx is non empty directed Element of bool the carrier of H

"\/" (xx,H) is Element of the carrier of H

f is Element of the carrier of H

{f} is non empty trivial finite V53(1) Element of bool the carrier of H

{f} "/\" (proj2 a) is Element of bool the carrier of H

H is non empty V70() reflexive up-complete non void RelStr

a is non empty V70() reflexive up-complete non void RelStr

[:H,a:] is non empty strict V70() reflexive non void RelStr

the carrier of [:H,a:] is non empty set

bool the carrier of [:H,a:] is non empty cup-closed diff-closed preBoolean set

X is non empty directed Element of bool the carrier of [:H,a:]

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

proj1 X is Element of bool the carrier of H

the carrier of a is non empty set

bool the carrier of a is non empty cup-closed diff-closed preBoolean set

proj2 X is Element of bool the carrier of a

X1 is non empty directed Element of bool the carrier of H

f is Element of the carrier of H

xx is non empty directed Element of bool the carrier of a

h is Element of the carrier of a

[f,h] is V1() Element of the carrier of [:H,a:]

{f,h} is non empty finite set

{f} is non empty trivial finite V53(1) set

{{f,h},{f}} is non empty finite V50() set

a is Element of the carrier of [:H,a:]

[: the carrier of H, the carrier of a:] is non empty Relation-like set

a `1 is Element of the carrier of H

a `2 is Element of the carrier of a

[(a `1),(a `2)] is V1() Element of the carrier of [:H,a:]

{(a `1),(a `2)} is non empty finite set

{(a `1)} is non empty trivial finite V53(1) set

{{(a `1),(a `2)},{(a `1)}} is non empty finite V50() set

H is non empty V70() reflexive antisymmetric non void RelStr

a is non empty V70() reflexive antisymmetric non void RelStr

[:H,a:] is non empty strict V70() reflexive antisymmetric non void RelStr

the carrier of a is non empty set

bool the carrier of a is non empty cup-closed diff-closed preBoolean set

the non empty directed Element of bool the carrier of a is non empty directed Element of bool the carrier of a

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

X1 is non empty directed Element of bool the carrier of H

the carrier of [:H,a:] is non empty set

[:X1, the non empty directed Element of bool the carrier of a:] is non empty Relation-like directed Element of bool the carrier of [:H,a:]

bool the carrier of [:H,a:] is non empty cup-closed diff-closed preBoolean set

xx is Element of the carrier of [:H,a:]

xx `1 is Element of the carrier of H

[: the carrier of H, the carrier of a:] is non empty Relation-like set

xx `2 is Element of the carrier of a

[(xx `1),(xx `2)] is V1() Element of the carrier of [:H,a:]

{(xx `1),(xx `2)} is non empty finite set

{(xx `1)} is non empty trivial finite V53(1) set

{{(xx `1),(xx `2)},{(xx `1)}} is non empty finite V50() set

"\/" ( the non empty directed Element of bool the carrier of a,a) is Element of the carrier of a

f is Element of the carrier of H

[f,("\/" ( the non empty directed Element of bool the carrier of a,a))] is V1() Element of the carrier of [:H,a:]

{f,("\/" ( the non empty directed Element of bool the carrier of a,a))} is non empty finite set

{f} is non empty trivial finite V53(1) set

{{f,("\/" ( the non empty directed Element of bool the carrier of a,a))},{f}} is non empty finite V50() set

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

the non empty directed Element of bool the carrier of H is non empty directed Element of bool the carrier of H

the carrier of a is non empty set

bool the carrier of a is non empty cup-closed diff-closed preBoolean set

X1 is non empty directed Element of bool the carrier of a

the carrier of [:H,a:] is non empty set

[: the non empty directed Element of bool the carrier of H,X1:] is non empty Relation-like directed Element of bool the carrier of [:H,a:]

bool the carrier of [:H,a:] is non empty cup-closed diff-closed preBoolean set

xx is Element of the carrier of [:H,a:]

"\/" ( the non empty directed Element of bool the carrier of H,H) is Element of the carrier of H

xx `2 is Element of the carrier of a

[: the carrier of H, the carrier of a:] is non empty Relation-like set

xx `1 is Element of the carrier of H

[(xx `1),(xx `2)] is V1() Element of the carrier of [:H,a:]

{(xx `1),(xx `2)} is non empty finite set

{(xx `1)} is non empty trivial finite V53(1) set

{{(xx `1),(xx `2)},{(xx `1)}} is non empty finite V50() set

f is Element of the carrier of a

[("\/" ( the non empty directed Element of bool the carrier of H,H)),f] is V1() Element of the carrier of [:H,a:]

{("\/" ( the non empty directed Element of bool the carrier of H,H)),f} is non empty finite set

{("\/" ( the non empty directed Element of bool the carrier of H,H))} is non empty trivial finite V53(1) set

{{("\/" ( the non empty directed Element of bool the carrier of H,H)),f},{("\/" ( the non empty directed Element of bool the carrier of H,H))}} is non empty finite V50() set

H is non empty V70() reflexive antisymmetric up-complete non void RelStr

[:H,H:] is non empty strict V70() reflexive antisymmetric up-complete non void RelStr

the carrier of [:H,H:] is non empty set

bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of [:H,H:]

"\/" (a,[:H,H:]) is Element of the carrier of [:H,H:]

proj1 a is Element of bool the carrier of H

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

"\/" ((proj1 a),H) is Element of the carrier of H

proj2 a is Element of bool the carrier of H

"\/" ((proj2 a),H) is Element of the carrier of H

[("\/" ((proj1 a),H)),("\/" ((proj2 a),H))] is V1() Element of the carrier of [:H,H:]

{("\/" ((proj1 a),H)),("\/" ((proj2 a),H))} is non empty finite set

{("\/" ((proj1 a),H))} is non empty trivial finite V53(1) set

{{("\/" ((proj1 a),H)),("\/" ((proj2 a),H))},{("\/" ((proj1 a),H))}} is non empty finite V50() set

xx is non empty set

[:xx,xx:] is non empty Relation-like set

bool [:xx,xx:] is non empty cup-closed diff-closed preBoolean set

X is non empty directed Element of bool the carrier of H

h is set

a is set

[h,a] is V1() set

{h,a} is non empty finite set

{h} is non empty trivial finite V53(1) set

{{h,a},{h}} is non empty finite V50() set

X1 is non empty directed Element of bool the carrier of H

Y is Element of the carrier of H

z is Element of the carrier of H

y is set

[y,z] is V1() set

{y,z} is non empty finite set

{y} is non empty trivial finite V53(1) set

{{y,z},{y}} is non empty finite V50() set

y is Element of the carrier of H

[y,Y] is V1() Element of the carrier of [:H,H:]

{y,Y} is non empty finite set

{y} is non empty trivial finite V53(1) set

{{y,Y},{y}} is non empty finite V50() set

z1 is Element of X

[z1,z] is V1() Element of the carrier of [:H,H:]

{z1,z} is non empty finite set

{z1} is non empty trivial finite V53(1) set

{{z1,z},{z1}} is non empty finite V50() set

"\/" (X1,H) is Element of the carrier of H

y is Element of the carrier of H

z is Element of the carrier of H

y is set

[z,y] is V1() set

{z,y} is non empty finite set

{z} is non empty trivial finite V53(1) set

{{z,y},{z}} is non empty finite V50() set

[y,Y] is V1() Element of the carrier of [:H,H:]

{y,Y} is non empty finite set

{y} is non empty trivial finite V53(1) set

{{y,Y},{y}} is non empty finite V50() set

z1 is Element of X1

[z,z1] is V1() Element of the carrier of [:H,H:]

{z,z1} is non empty finite set

{{z,z1},{z}} is non empty finite V50() set

"\/" (X,H) is Element of the carrier of H

[("\/" (X,H)),("\/" (X1,H))] is V1() Element of the carrier of [:H,H:]

{("\/" (X,H)),("\/" (X1,H))} is non empty finite set

{("\/" (X,H))} is non empty trivial finite V53(1) set

{{("\/" (X,H)),("\/" (X1,H))},{("\/" (X,H))}} is non empty finite V50() set

[:X,X1:] is non empty Relation-like directed Element of bool the carrier of [:H,H:]

f is non empty Relation-like xx -defined xx -valued Element of bool [:xx,xx:]

z is non empty Element of bool the carrier of H

y is non empty Element of bool the carrier of H

[:z,y:] is non empty Relation-like Element of bool the carrier of [:H,H:]

"\/" ([:z,y:],[:H,H:]) is Element of the carrier of [:H,H:]

H is RelStr

the carrier of H is set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is RelStr

the carrier of a is set

[: the carrier of H, the carrier of a:] is Relation-like set

bool [: the carrier of H, the carrier of a:] is non empty cup-closed diff-closed preBoolean set

X is Element of bool the carrier of H

downarrow X is Element of bool the carrier of H

X1 is Relation-like the carrier of H -defined the carrier of a -valued Function-like V33( the carrier of H, the carrier of a) Element of bool [: the carrier of H, the carrier of a:]

X1 .: (downarrow X) is Element of bool the carrier of a

bool the carrier of a is non empty cup-closed diff-closed preBoolean set

X1 .: X is Element of bool the carrier of a

downarrow (X1 .: X) is Element of bool the carrier of a

xx is set

dom X1 is Element of bool the carrier of H

f is set

X1 . f is set

h is non empty RelStr

the carrier of h is non empty set

y is Element of the carrier of h

Y is Element of the carrier of h

a is non empty RelStr

the carrier of a is non empty set

[: the carrier of h, the carrier of a:] is non empty Relation-like set

bool [: the carrier of h, the carrier of a:] is non empty cup-closed diff-closed preBoolean set

z is non empty Relation-like the carrier of h -defined the carrier of a -valued Function-like V31( the carrier of h) V33( the carrier of h, the carrier of a) Element of bool [: the carrier of h, the carrier of a:]

z . y is Element of the carrier of a

z . Y is Element of the carrier of a

X1 . Y is set

y is Element of the carrier of a

z1 is Element of the carrier of a

H is RelStr

the carrier of H is set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is RelStr

the carrier of a is set

[: the carrier of H, the carrier of a:] is Relation-like set

bool [: the carrier of H, the carrier of a:] is non empty cup-closed diff-closed preBoolean set

X is Element of bool the carrier of H

uparrow X is Element of bool the carrier of H

X1 is Relation-like the carrier of H -defined the carrier of a -valued Function-like V33( the carrier of H, the carrier of a) Element of bool [: the carrier of H, the carrier of a:]

X1 .: (uparrow X) is Element of bool the carrier of a

bool the carrier of a is non empty cup-closed diff-closed preBoolean set

X1 .: X is Element of bool the carrier of a

uparrow (X1 .: X) is Element of bool the carrier of a

xx is set

dom X1 is Element of bool the carrier of H

f is set

X1 . f is set

h is non empty RelStr

the carrier of h is non empty set

y is Element of the carrier of h

Y is Element of the carrier of h

a is non empty RelStr

the carrier of a is non empty set

[: the carrier of h, the carrier of a:] is non empty Relation-like set

bool [: the carrier of h, the carrier of a:] is non empty cup-closed diff-closed preBoolean set

z is non empty Relation-like the carrier of h -defined the carrier of a -valued Function-like V31( the carrier of h) V33( the carrier of h, the carrier of a) Element of bool [: the carrier of h, the carrier of a:]

z . y is Element of the carrier of a

z . Y is Element of the carrier of a

X1 . Y is set

z1 is Element of the carrier of a

y is Element of the carrier of a

H is non empty trivial finite 1 -element V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() connected up-complete /\-complete non void with_suprema with_infima complete RelStr

the carrier of H is non empty trivial finite V53(1) set

a is Element of the carrier of H

X is Element of the carrier of H

X1 is Element of the carrier of H

X "\/" X1 is Element of the carrier of H

a "/\" (X "\/" X1) is Element of the carrier of H

a "/\" X is Element of the carrier of H

a "/\" X1 is Element of the carrier of H

(a "/\" X) "\/" (a "/\" X1) is Element of the carrier of H

the carrier of H is non empty trivial finite V53(1) set

a is Element of the carrier of H

X is Element of the carrier of H

a "\/" X is Element of the carrier of H

Top H is Element of the carrier of H

"/\" ({},H) is Element of the carrier of H

a "/\" X is Element of the carrier of H

Bottom H is Element of the carrier of H

"\/" ({},H) is Element of the carrier of H

the non empty trivial finite 1 -element strict V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() connected up-complete /\-complete distributive Heyting complemented Boolean non void with_suprema with_infima complete RelStr is non empty trivial finite 1 -element strict V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() connected up-complete /\-complete distributive Heyting complemented Boolean non void with_suprema with_infima complete RelStr

H is non empty V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() up-complete /\-complete distributive non void with_suprema with_infima complete RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is Element of the carrier of H

{a} is non empty trivial finite V53(1) Element of bool the carrier of H

X is finite Element of bool the carrier of H

{a} "/\" X is Element of bool the carrier of H

"\/" (({a} "/\" X),H) is Element of the carrier of H

"\/" (X,H) is Element of the carrier of H

a "/\" ("\/" (X,H)) is Element of the carrier of H

X1 is Element of bool the carrier of H

"\/" (X1,H) is Element of the carrier of H

a "/\" ("\/" (X1,H)) is Element of the carrier of H

{a} "/\" X1 is Element of bool the carrier of H

"\/" (({a} "/\" X1),H) is Element of the carrier of H

Bottom H is Element of the carrier of H

"\/" ({},H) is Element of the carrier of H

{} H is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V39() V40() V41() V43() V44() V45() finite finite-yielding V50() V51() V53( {} ) strongly_connected directed filtered Element of bool the carrier of H

{a} "/\" ({} H) is Element of bool the carrier of H

X1 is set

xx is set

{X1} is non empty trivial finite V53(1) set

xx \/ {X1} is non empty set

f is Element of the carrier of H

{f} is non empty trivial finite V53(1) Element of bool the carrier of H

h is Element of bool the carrier of H

"\/" (h,H) is Element of the carrier of H

a "/\" ("\/" (h,H)) is Element of the carrier of H

{a} "/\" h is Element of bool the carrier of H

"\/" (({a} "/\" h),H) is Element of the carrier of H

a is Element of bool the carrier of H

"\/" (a,H) is Element of the carrier of H

a "/\" ("\/" (a,H)) is Element of the carrier of H

{a} "/\" a is Element of bool the carrier of H

"\/" (({a} "/\" a),H) is Element of the carrier of H

a is Element of bool the carrier of H

"\/" (a,H) is Element of the carrier of H

a "/\" ("\/" (a,H)) is Element of the carrier of H

{a} "/\" a is Element of bool the carrier of H

"\/" (({a} "/\" a),H) is Element of the carrier of H

{a} "/\" {f} is non empty Element of bool the carrier of H

({a} "/\" a) \/ ({a} "/\" {f}) is non empty Element of bool the carrier of H

a "/\" f is Element of the carrier of H

{(a "/\" f)} is non empty trivial finite V53(1) Element of bool the carrier of H

({a} "/\" a) \/ {(a "/\" f)} is non empty Element of bool the carrier of H

"\/" (xx,H) is Element of the carrier of H

"\/" ({X1},H) is Element of the carrier of H

("\/" (xx,H)) "\/" ("\/" ({X1},H)) is Element of the carrier of H

a "/\" (("\/" (xx,H)) "\/" ("\/" ({X1},H))) is Element of the carrier of H

a "/\" ("\/" ({X1},H)) is Element of the carrier of H

("\/" (({a} "/\" a),H)) "\/" (a "/\" ("\/" ({X1},H))) is Element of the carrier of H

("\/" (({a} "/\" a),H)) "\/" (a "/\" f) is Element of the carrier of H

"\/" ({(a "/\" f)},H) is Element of the carrier of H

("\/" (({a} "/\" a),H)) "\/" ("\/" ({(a "/\" f)},H)) is Element of the carrier of H

X1 is Element of bool the carrier of H

"\/" (X1,H) is Element of the carrier of H

a "/\" ("\/" (X1,H)) is Element of the carrier of H

{a} "/\" X1 is Element of bool the carrier of H

"\/" (({a} "/\" X1),H) is Element of the carrier of H

H is non empty V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() up-complete /\-complete distributive non void with_suprema with_infima complete RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is Element of the carrier of H

{a} is non empty trivial finite V53(1) Element of bool the carrier of H

X is finite Element of bool the carrier of H

{a} "\/" X is Element of bool the carrier of H

"/\" (({a} "\/" X),H) is Element of the carrier of H

"/\" (X,H) is Element of the carrier of H

a "\/" ("/\" (X,H)) is Element of the carrier of H

X1 is Element of bool the carrier of H

"/\" (X1,H) is Element of the carrier of H

a "\/" ("/\" (X1,H)) is Element of the carrier of H

{a} "\/" X1 is Element of bool the carrier of H

"/\" (({a} "\/" X1),H) is Element of the carrier of H

Top H is Element of the carrier of H

"/\" ({},H) is Element of the carrier of H

{} H is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V39() V40() V41() V43() V44() V45() finite finite-yielding V50() V51() V53( {} ) strongly_connected directed filtered Element of bool the carrier of H

{a} "\/" ({} H) is Element of bool the carrier of H

X1 is set

xx is set

{X1} is non empty trivial finite V53(1) set

xx \/ {X1} is non empty set

f is Element of the carrier of H

{f} is non empty trivial finite V53(1) Element of bool the carrier of H

h is Element of bool the carrier of H

"/\" (h,H) is Element of the carrier of H

a "\/" ("/\" (h,H)) is Element of the carrier of H

{a} "\/" h is Element of bool the carrier of H

"/\" (({a} "\/" h),H) is Element of the carrier of H

a is Element of bool the carrier of H

"/\" (a,H) is Element of the carrier of H

a "\/" ("/\" (a,H)) is Element of the carrier of H

{a} "\/" a is Element of bool the carrier of H

"/\" (({a} "\/" a),H) is Element of the carrier of H

a is Element of bool the carrier of H

"/\" (a,H) is Element of the carrier of H

a "\/" ("/\" (a,H)) is Element of the carrier of H

{a} "\/" a is Element of bool the carrier of H

"/\" (({a} "\/" a),H) is Element of the carrier of H

{a} "\/" {f} is non empty Element of bool the carrier of H

({a} "\/" a) \/ ({a} "\/" {f}) is non empty Element of bool the carrier of H

a "\/" f is Element of the carrier of H

{(a "\/" f)} is non empty trivial finite V53(1) Element of bool the carrier of H

({a} "\/" a) \/ {(a "\/" f)} is non empty Element of bool the carrier of H

"/\" (xx,H) is Element of the carrier of H

"/\" ({X1},H) is Element of the carrier of H

("/\" (xx,H)) "/\" ("/\" ({X1},H)) is Element of the carrier of H

a "\/" (("/\" (xx,H)) "/\" ("/\" ({X1},H))) is Element of the carrier of H

a "\/" ("/\" ({X1},H)) is Element of the carrier of H

("/\" (({a} "\/" a),H)) "/\" (a "\/" ("/\" ({X1},H))) is Element of the carrier of H

("/\" (({a} "\/" a),H)) "/\" (a "\/" f) is Element of the carrier of H

"/\" ({(a "\/" f)},H) is Element of the carrier of H

("/\" (({a} "\/" a),H)) "/\" ("/\" ({(a "\/" f)},H)) is Element of the carrier of H

X1 is Element of bool the carrier of H

"/\" (X1,H) is Element of the carrier of H

a "\/" ("/\" (X1,H)) is Element of the carrier of H

{a} "\/" X1 is Element of bool the carrier of H

"/\" (({a} "\/" X1),H) is Element of the carrier of H

H is non empty V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() up-complete /\-complete distributive non void with_suprema with_infima complete RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

a is Element of the carrier of H

a "/\" is non empty Relation-like the carrier of H -defined the carrier of H -valued Function-like V31( the carrier of H) V33( the carrier of H, the carrier of H) monotone Element of bool [: the carrier of H, the carrier of H:]

[: the carrier of H, the carrier of H:] is non empty Relation-like set

bool [: the carrier of H, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

X is finite Element of bool the carrier of H

(a "/\") .: X is finite Element of bool the carrier of H

"\/" (((a "/\") .: X),H) is Element of the carrier of H

"\/" (X,H) is Element of the carrier of H

(a "/\") . ("\/" (X,H)) is Element of the carrier of H

{ (a "/\" b

"\/" ( { (a "/\" b

{a} is non empty trivial finite V53(1) Element of bool the carrier of H

{a} "/\" X is Element of bool the carrier of H

"\/" (({a} "/\" X),H) is Element of the carrier of H

a "/\" ("\/" (X,H)) is Element of the carrier of H

F

the carrier of F

F

the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

the mapping of F

[: the carrier of F

bool [: the carrier of F

H is Element of the carrier of F

the mapping of F

F

H is non empty Relation-like the carrier of F

NetStr(# the carrier of F

the carrier of NetStr(# the carrier of F

the InternalRel of NetStr(# the carrier of F

[: the carrier of NetStr(# the carrier of F

bool [: the carrier of NetStr(# the carrier of F

RelStr(# the carrier of NetStr(# the carrier of F

[#] F

bool the carrier of F

[#] NetStr(# the carrier of F

bool the carrier of NetStr(# the carrier of F

X is non empty directed NetStr over F

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 bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: 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 non empty strict RelStr

the mapping of X is non empty Relation-like the carrier of X -defined the carrier of F

[: the carrier of X, the carrier of F

bool [: the carrier of X, the carrier of F

X1 is Element of the carrier of X

the mapping of X . X1 is Element of the carrier of F

the mapping of F

F

H is non empty RelStr

the carrier of H is non empty set

a is non empty directed NetStr over H

netmap (a,H) is non empty Relation-like the carrier of a -defined the carrier of H -valued Function-like V31( the carrier of a) V33( the carrier of a, the carrier of H) Element of bool [: the carrier of a, the carrier of H:]

the carrier of a is non empty set

[: the carrier of a, the carrier of H:] is non empty Relation-like set

bool [: the carrier of a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

the mapping of a is non empty Relation-like the carrier of a -defined the carrier of H -valued Function-like V31( the carrier of a) V33( the carrier of a, the carrier of H) Element of bool [: the carrier of a, the carrier of H:]

rng (netmap (a,H)) is non empty Element of bool the carrier of H

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

X1 is Element of the carrier of H

xx is Element of the carrier of H

dom (netmap (a,H)) is non empty Element of bool the carrier of a

bool the carrier of a is non empty cup-closed diff-closed preBoolean set

f is set

(netmap (a,H)) . f is set

h is set

(netmap (a,H)) . h is set

a is Element of the carrier of a

a . a is Element of the carrier of H

the mapping of a . a is Element of the carrier of H

Y is Element of the carrier of a

y is Element of the carrier of a

a . y is Element of the carrier of H

the mapping of a . y is Element of the carrier of H

z is Element of the carrier of a

[#] a is non empty non proper lower upper Element of bool the carrier of a

y is Element of the carrier of a

(netmap (a,H)) . y is Element of the carrier of H

z1 is Element of the carrier of H

a . y is Element of the carrier of H

the mapping of a . y is Element of the carrier of H

H is non empty V70() reflexive non void RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

the InternalRel of H is non empty Relation-like the carrier of H -defined the carrier of H -valued V23() V31( the carrier of H) V33( the carrier of H, the carrier of H) Element of bool [: the carrier of H, the carrier of H:]

[: the carrier of H, the carrier of H:] is non empty Relation-like set

bool [: the carrier of H, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of H

[:a, the carrier of H:] is non empty Relation-like set

bool [:a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

the InternalRel of H |_2 a is Relation-like a -defined a -valued Element of bool [:a,a:]

[:a,a:] is non empty Relation-like set

bool [:a,a:] is non empty cup-closed diff-closed preBoolean set

the InternalRel of H /\ [:a,a:] is Relation-like the carrier of H -defined the carrier of H -valued set

X is non empty Relation-like a -defined the carrier of H -valued Function-like V31(a) V33(a, the carrier of H) Element of bool [:a, the carrier of H:]

NetStr(# a,( the InternalRel of H |_2 a),X #) is non empty strict NetStr over H

the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #) is non empty set

xx is Element of the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #)

[#] NetStr(# a,( the InternalRel of H |_2 a),X #) is non empty non proper lower upper Element of bool the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #)

bool the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #) is non empty cup-closed diff-closed preBoolean set

f is Element of the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #)

h is Element of a

a is Element of a

y is Element of the carrier of H

Y is Element of the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #)

the InternalRel of NetStr(# a,( the InternalRel of H |_2 a),X #) is Relation-like the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #) -defined the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #) -valued Element of bool [: the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #), the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #):]

[: the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #), the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #):] is non empty Relation-like set

bool [: the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #), the carrier of NetStr(# a,( the InternalRel of H |_2 a),X #):] is non empty cup-closed diff-closed preBoolean set

z is SubRelStr of H

H is non empty V70() reflexive non void RelStr

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

the InternalRel of H is non empty Relation-like the carrier of H -defined the carrier of H -valued V23() V31( the carrier of H) V33( the carrier of H, the carrier of H) Element of bool [: the carrier of H, the carrier of H:]

[: the carrier of H, the carrier of H:] is non empty Relation-like set

bool [: the carrier of H, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

a is non empty directed Element of bool the carrier of H

[:a, the carrier of H:] is non empty Relation-like set

bool [:a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

id a is non empty Relation-like a -defined a -valued Function-like one-to-one V31(a) V33(a,a) Element of bool [:a,a:]

[:a,a:] is non empty Relation-like set

bool [:a,a:] is non empty cup-closed diff-closed preBoolean set

the InternalRel of H |_2 a is Relation-like a -defined a -valued Element of bool [:a,a:]

the InternalRel of H /\ [:a,a:] is Relation-like the carrier of H -defined the carrier of H -valued set

X is non empty Relation-like a -defined the carrier of H -valued Function-like V31(a) V33(a, the carrier of H) Element of bool [:a, the carrier of H:]

NetStr(# a,( the InternalRel of H |_2 a),X #) is non empty strict NetStr over H

X1 is non empty directed NetStr over H

the carrier of X1 is non empty set

xx is Element of the carrier of X1

X1 . xx is Element of the carrier of H

the mapping of X1 is non empty Relation-like the carrier of X1 -defined the carrier of H -valued Function-like V31( the carrier of X1) V33( the carrier of X1, the carrier of H) Element of bool [: the carrier of X1, the carrier of H:]

[: the carrier of X1, the carrier of H:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

the mapping of X1 . xx is Element of the carrier of H

f is Element of the carrier of X1

h is Element of the carrier of X1

X1 . h is Element of the carrier of H

the mapping of X1 . h is Element of the carrier of H

the InternalRel of X1 is Relation-like the carrier of X1 -defined the carrier of X1 -valued Element of bool [: the carrier of X1, the carrier of X1:]

[: the carrier of X1, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of X1:] is non empty cup-closed diff-closed preBoolean set

X . f is set

X . h is set

a is Element of the carrier of H

y is Element of the carrier of H

H is non empty RelStr

a is NetStr over H

the mapping of a is Relation-like the carrier of a -defined the carrier of H -valued Function-like V31( the carrier of a) V33( the carrier of a, the carrier of H) Element of bool [: the carrier of a, the carrier of H:]

the carrier of a is set

the carrier of H is non empty set

[: the carrier of a, the carrier of H:] is Relation-like set

bool [: the carrier of a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

\\/ ( the mapping of a,H) is Element of the carrier of H

a is set

H is non empty RelStr

the carrier of H is non empty set

[:a, the carrier of H:] is Relation-like set

bool [:a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

Fin a is non empty cup-closed diff-closed preBoolean set

[:(Fin a), the carrier of H:] is non empty Relation-like set

bool [:(Fin a), the carrier of H:] is non empty cup-closed diff-closed preBoolean set

X is Relation-like a -defined the carrier of H -valued Function-like V31(a) V33(a, the carrier of H) Element of bool [:a, the carrier of H:]

RelIncl (Fin a) is Relation-like Fin a -defined Fin a -valued V23() V26() V30() V31( Fin a) V33( Fin a, Fin a) Element of bool [:(Fin a),(Fin a):]

[:(Fin a),(Fin a):] is non empty Relation-like set

bool [:(Fin a),(Fin a):] is non empty cup-closed diff-closed preBoolean set

X1 is finite Element of Fin a

X .: X1 is finite Element of bool the carrier of H

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

"\/" ((X .: X1),H) is Element of the carrier of H

X1 is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),X1 #) is non empty strict NetStr over H

the carrier of NetStr(# (Fin a),(RelIncl (Fin a)),X1 #) is non empty set

f is Element of the carrier of NetStr(# (Fin a),(RelIncl (Fin a)),X1 #)

[#] NetStr(# (Fin a),(RelIncl (Fin a)),X1 #) is non empty non proper lower upper Element of bool the carrier of NetStr(# (Fin a),(RelIncl (Fin a)),X1 #)

bool the carrier of NetStr(# (Fin a),(RelIncl (Fin a)),X1 #) is non empty cup-closed diff-closed preBoolean set

h is Element of the carrier of NetStr(# (Fin a),(RelIncl (Fin a)),X1 #)

a is finite Element of Fin a

y is finite Element of Fin a

a \/ y is finite Element of Fin a

Y is Element of the carrier of NetStr(# (Fin a),(RelIncl (Fin a)),X1 #)

InclPoset (Fin a) is non empty strict V70() reflexive transitive antisymmetric non void RelStr

RelStr(# (Fin a),(RelIncl (Fin a)) #) is non empty strict V70() reflexive transitive antisymmetric non void RelStr

the carrier of (InclPoset (Fin a)) is non empty set

y is Element of the carrier of (InclPoset (Fin a))

z1 is Element of the carrier of (InclPoset (Fin a))

z is Element of the carrier of (InclPoset (Fin a))

f is non empty directed NetStr over H

X1 is non empty directed NetStr over H

xx is non empty directed NetStr over H

f is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),f #) is non empty strict NetStr over H

f is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),f #) is non empty strict NetStr over H

h is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),h #) is non empty strict NetStr over H

h is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),h #) is non empty strict NetStr over H

a is set

f . a is set

h . a is set

X .: a is Element of bool the carrier of H

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

"\/" ((X .: a),H) is Element of the carrier of H

H is non empty RelStr

the carrier of H is non empty set

a is set

[:a, the carrier of H:] is Relation-like set

bool [:a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

X is set

Fin a is non empty cup-closed diff-closed preBoolean set

X1 is Relation-like a -defined the carrier of H -valued Function-like V31(a) V33(a, the carrier of H) Element of bool [:a, the carrier of H:]

(H,a,X1) is non empty directed NetStr over H

the carrier of (H,a,X1) is non empty set

[:(Fin a), the carrier of H:] is non empty Relation-like set

bool [:(Fin a), the carrier of H:] is non empty cup-closed diff-closed preBoolean set

RelIncl (Fin a) is Relation-like Fin a -defined Fin a -valued V23() V26() V30() V31( Fin a) V33( Fin a, Fin a) Element of bool [:(Fin a),(Fin a):]

[:(Fin a),(Fin a):] is non empty Relation-like set

bool [:(Fin a),(Fin a):] is non empty cup-closed diff-closed preBoolean set

xx is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),xx #) is non empty strict NetStr over H

a is set

H is non empty V70() reflexive antisymmetric lower-bounded upper-bounded V134() up-complete /\-complete non void with_suprema with_infima complete RelStr

the carrier of H is non empty set

[:a, the carrier of H:] is Relation-like set

bool [:a, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

X is Relation-like a -defined the carrier of H -valued Function-like V31(a) V33(a, the carrier of H) Element of bool [:a, the carrier of H:]

(H,a,X) is non empty directed NetStr over H

the carrier of (H,a,X) is non empty set

X1 is Element of the carrier of (H,a,X)

xx is Element of the carrier of (H,a,X)

netmap ((H,a,X),H) is non empty Relation-like the carrier of (H,a,X) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,X)) V33( the carrier of (H,a,X), the carrier of H) Element of bool [: the carrier of (H,a,X), the carrier of H:]

[: the carrier of (H,a,X), the carrier of H:] is non empty Relation-like set

bool [: the carrier of (H,a,X), the carrier of H:] is non empty cup-closed diff-closed preBoolean set

the mapping of (H,a,X) is non empty Relation-like the carrier of (H,a,X) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,X)) V33( the carrier of (H,a,X), the carrier of H) Element of bool [: the carrier of (H,a,X), the carrier of H:]

(netmap ((H,a,X),H)) . X1 is set

(netmap ((H,a,X),H)) . xx is set

Fin a is non empty cup-closed diff-closed preBoolean set

[:(Fin a), the carrier of H:] is non empty Relation-like set

bool [:(Fin a), the carrier of H:] is non empty cup-closed diff-closed preBoolean set

RelIncl (Fin a) is Relation-like Fin a -defined Fin a -valued V23() V26() V30() V31( Fin a) V33( Fin a, Fin a) Element of bool [:(Fin a),(Fin a):]

[:(Fin a),(Fin a):] is non empty Relation-like set

bool [:(Fin a),(Fin a):] is non empty cup-closed diff-closed preBoolean set

f is non empty Relation-like Fin a -defined the carrier of H -valued Function-like V31( Fin a) V33( Fin a, the carrier of H) Element of bool [:(Fin a), the carrier of H:]

NetStr(# (Fin a),(RelIncl (Fin a)),f #) is non empty strict NetStr over H

f . X1 is set

X .: X1 is Element of bool the carrier of H

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

"\/" ((X .: X1),H) is Element of the carrier of H

InclPoset (Fin a) is non empty strict V70() reflexive transitive antisymmetric non void RelStr

RelStr(# (Fin a),(RelIncl (Fin a)) #) is non empty strict V70() reflexive transitive antisymmetric non void RelStr

the carrier of (InclPoset (Fin a)) is non empty set

X .: xx is Element of bool the carrier of H

a is Element of the carrier of (InclPoset (Fin a))

y is Element of the carrier of (InclPoset (Fin a))

"\/" ((X .: xx),H) is Element of the carrier of H

h is Element of the carrier of H

Y is Element of the carrier of H

z is Element of the carrier of H

(netmap ((H,a,X),H)) . X1 is Element of the carrier of H

(netmap ((H,a,X),H)) . xx is Element of the carrier of H

H is non empty RelStr

the carrier of H is non empty set

X is non empty NetStr over H

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 bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: 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 non empty strict RelStr

the mapping of X is non empty Relation-like the carrier of X -defined the carrier of H -valued Function-like V31( the carrier of X) V33( the carrier of X, the carrier of H) Element of bool [: the carrier of X, the carrier of H:]

[: the carrier of X, the carrier of H:] is non empty Relation-like set

bool [: the carrier of X, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

a is Element of the carrier of H

X1 is Element of the carrier of X

the mapping of X . X1 is set

the mapping of X . X1 is Element of the carrier of H

a "/\" ( the mapping of X . X1) is Element of the carrier of H

X1 is non empty Relation-like the carrier of X -defined the carrier of H -valued Function-like V31( the carrier of X) V33( the carrier of X, the carrier of H) Element of bool [: the carrier of X, the carrier of H:]

X1 is non empty Relation-like the carrier of X -defined the carrier of H -valued Function-like V31( the carrier of X) V33( the carrier of X, the carrier of H) Element of bool [: the carrier of X, the carrier of H:]

NetStr(# the carrier of X, the InternalRel of X,X1 #) is non empty strict NetStr over H

the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #) is non empty set

the InternalRel of NetStr(# the carrier of X, the InternalRel of X,X1 #) is Relation-like the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #) -defined the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #) -valued Element of bool [: the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #):]

[: the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #):] is non empty Relation-like set

bool [: the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #):] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the InternalRel of NetStr(# the carrier of X, the InternalRel of X,X1 #) #) is non empty strict RelStr

the mapping of NetStr(# the carrier of X, the InternalRel of X,X1 #) is non empty Relation-like the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #) -defined the carrier of H -valued Function-like V31( the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #)) V33( the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of H) Element of bool [: the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of H:]

[: the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of H:] is non empty Relation-like set

bool [: the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #), the carrier of H:] is non empty cup-closed diff-closed preBoolean set

xx is Element of the carrier of NetStr(# the carrier of X, the InternalRel of X,X1 #)

the mapping of X . xx is set

the mapping of NetStr(# the carrier of X, the InternalRel of X,X1 #) . xx is set

X1 is strict NetStr over H

the carrier of X1 is set

the InternalRel of X1 is Relation-like the carrier of X1 -defined the carrier of X1 -valued Element of bool [: the carrier of X1, the carrier of X1:]

[: the carrier of X1, the carrier of X1:] is Relation-like set

bool [: the carrier of X1, the carrier of X1:] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of X1, the InternalRel of X1 #) is strict RelStr

the mapping of X1 is Relation-like the carrier of X1 -defined the carrier of H -valued Function-like V31( the carrier of X1) V33( the carrier of X1, the carrier of H) Element of bool [: the carrier of X1, the carrier of H:]

[: the carrier of X1, the carrier of H:] is Relation-like set

bool [: the carrier of X1, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

xx is strict NetStr over H

the carrier of xx is set

the InternalRel of xx is Relation-like the carrier of xx -defined the carrier of xx -valued Element of bool [: the carrier of xx, the carrier of xx:]

[: the carrier of xx, the carrier of xx:] is Relation-like set

bool [: the carrier of xx, the carrier of xx:] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of xx, the InternalRel of xx #) is strict RelStr

the mapping of xx is Relation-like the carrier of xx -defined the carrier of H -valued Function-like V31( the carrier of xx) V33( the carrier of xx, the carrier of H) Element of bool [: the carrier of xx, the carrier of H:]

[: the carrier of xx, the carrier of H:] is Relation-like set

bool [: the carrier of xx, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

f is non empty set

[:f, the carrier of H:] is non empty Relation-like set

bool [:f, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

h is non empty Relation-like f -defined the carrier of H -valued Function-like V31(f) V33(f, the carrier of H) Element of bool [:f, the carrier of H:]

a is non empty Relation-like f -defined the carrier of H -valued Function-like V31(f) V33(f, the carrier of H) Element of bool [:f, the carrier of H:]

y is Element of f

h . y is Element of the carrier of H

a . y is Element of the carrier of H

the mapping of X . y is set

Y is Element of the carrier of H

a "/\" Y is Element of the carrier of H

z is Element of the carrier of H

a "/\" z is Element of the carrier of H

H is non empty RelStr

the carrier of H is non empty set

a is non empty NetStr over H

the carrier of a is non empty set

X is Element of the carrier of H

(H,X,a) is strict NetStr over H

the carrier of (H,X,a) is set

X1 is set

the InternalRel of (H,X,a) is Relation-like the carrier of (H,X,a) -defined the carrier of (H,X,a) -valued Element of bool [: the carrier of (H,X,a), the carrier of (H,X,a):]

[: the carrier of (H,X,a), the carrier of (H,X,a):] is Relation-like set

bool [: the carrier of (H,X,a), the carrier of (H,X,a):] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of (H,X,a), the InternalRel of (H,X,a) #) is strict RelStr

the InternalRel of a is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty Relation-like set

bool [: the carrier of a, the carrier of a:] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of a, the InternalRel of a #) is non empty strict RelStr

H is non empty RelStr

the carrier of H is non empty set

a is Element of the carrier of H

X is non empty NetStr over H

(H,a,X) is strict NetStr over H

the carrier of (H,a,X) is set

the InternalRel of (H,a,X) is Relation-like the carrier of (H,a,X) -defined the carrier of (H,a,X) -valued Element of bool [: the carrier of (H,a,X), the carrier of (H,a,X):]

[: the carrier of (H,a,X), the carrier of (H,a,X):] is Relation-like set

bool [: the carrier of (H,a,X), the carrier of (H,a,X):] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of (H,a,X), the InternalRel of (H,a,X) #) is strict RelStr

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 bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: 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 non empty strict RelStr

H is non empty RelStr

the carrier of H is non empty set

a is Element of the carrier of H

X is non empty directed NetStr over H

(H,a,X) is non empty strict NetStr over H

the carrier of (H,a,X) is non empty set

the InternalRel of (H,a,X) is Relation-like the carrier of (H,a,X) -defined the carrier of (H,a,X) -valued Element of bool [: the carrier of (H,a,X), the carrier of (H,a,X):]

[: the carrier of (H,a,X), the carrier of (H,a,X):] is non empty Relation-like set

bool [: the carrier of (H,a,X), the carrier of (H,a,X):] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of (H,a,X), the InternalRel of (H,a,X) #) is non empty strict RelStr

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 bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: 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 non empty strict RelStr

[#] X is non empty non proper lower upper Element of bool the carrier of X

bool the carrier of X is non empty cup-closed diff-closed preBoolean set

[#] (H,a,X) is non empty non proper lower upper Element of bool the carrier of (H,a,X)

bool the carrier of (H,a,X) is non empty cup-closed diff-closed preBoolean set

H is non empty RelStr

the carrier of H is non empty set

a is Element of the carrier of H

{a} is non empty trivial finite V53(1) Element of bool the carrier of H

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

X is non empty NetStr over H

(H,a,X) is non empty strict NetStr over H

the mapping of (H,a,X) is non empty Relation-like the carrier of (H,a,X) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,X)) V33( the carrier of (H,a,X), the carrier of H) Element of bool [: the carrier of (H,a,X), the carrier of H:]

the carrier of (H,a,X) is non empty set

[: the carrier of (H,a,X), the carrier of H:] is non empty Relation-like set

bool [: the carrier of (H,a,X), the carrier of H:] is non empty cup-closed diff-closed preBoolean set

rng the mapping of (H,a,X) is non empty Element of bool the carrier of H

the mapping of X is non empty Relation-like the carrier of X -defined the carrier of H -valued Function-like V31( the carrier of X) V33( the carrier of X, the carrier of H) Element of bool [: the carrier of X, the carrier of H:]

the carrier of X is non empty set

[: the carrier of X, the carrier of H:] is non empty Relation-like set

bool [: the carrier of X, the carrier of H:] is non empty cup-closed diff-closed preBoolean set

rng the mapping of X is non empty Element of bool the carrier of H

{a} "/\" (rng the mapping of X) is non empty Element of bool the carrier of H

{ (a "/\" b

the InternalRel of (H,a,X) is Relation-like the carrier of (H,a,X) -defined the carrier of (H,a,X) -valued Element of bool [: the carrier of (H,a,X), the carrier of (H,a,X):]

[: the carrier of (H,a,X), the carrier of (H,a,X):] is non empty Relation-like set

bool [: the carrier of (H,a,X), the carrier of (H,a,X):] is non empty cup-closed diff-closed preBoolean set

RelStr(# the carrier of (H,a,X), the InternalRel of (H,a,X) #) is non empty strict RelStr

the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: 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 non empty strict RelStr

dom the mapping of (H,a,X) is non empty Element of bool the carrier of (H,a,X)