:: WELLSET1 semantic presentation

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

N is set

M is Relation-like set

field M is set

dom M is set

rng M is set

(dom M) \/ (rng M) is set

D is set

[N,D] is set

{N,D} is non empty set

{N} is non empty set

{{N,D},{N}} is non empty set

F is set

[F,N] is set

{F,N} is non empty set

{F} is non empty set

{{F,N},{F}} is non empty set

N is set

M is set

[:N,M:] is Relation-like set

N \/ M is set

D is Relation-like set

field D is set

the Element of N is Element of N

the Element of M is Element of M

Z is set

H is set

[Z,H] is set

{Z,H} is non empty set

{Z} is non empty set

{{Z,H},{Z}} is non empty set

[H,Z] is set

{H,Z} is non empty set

{H} is non empty set

{{H,Z},{H}} is non empty set

Z is set

[Z, the Element of M] is set

{Z, the Element of M} is non empty set

{Z} is non empty set

{{Z, the Element of M},{Z}} is non empty set

[ the Element of N,Z] is set

{ the Element of N,Z} is non empty set

{ the Element of N} is non empty set

{{ the Element of N,Z},{ the Element of N}} is non empty set

F

N is set

M is set

F is Relation-like set

D is set

S is Relation-like set

N is set

M is Relation-like set

D is set

F is Relation-like set

S is Relation-like set

D is Relation-like set

N is set

M is set

[M,N] is set

{M,N} is non empty set

{M} is non empty set

{{M,N},{M}} is non empty set

D is Relation-like set

field D is set

D -Seg M is set

Coim (D,M) is set

(Coim (D,M)) \ {M} is Element of bool (Coim (D,M))

bool (Coim (D,M)) is non empty set

[N,M] is set

{N,M} is non empty set

{N} is non empty set

{{N,M},{N}} is non empty set

N is set

M is set

[M,N] is set

{M,N} is non empty set

{M} is non empty set

{{M,N},{M}} is non empty set

D is Relation-like set

field D is set

D -Seg M is set

Coim (D,M) is set

(Coim (D,M)) \ {M} is Element of bool (Coim (D,M))

bool (Coim (D,M)) is non empty set

[N,M] is set

{N,M} is non empty set

{N} is non empty set

{{N,M},{N}} is non empty set

N is Relation-like Function-like set

M is set

union M is set

[:(union M),(union M):] is Relation-like set

bool [:(union M),(union M):] is non empty set

F is set

S is Relation-like set

Z is Relation-like set

field Z is set

H is set

W0 is set

[H,W0] is set

{H,W0} is non empty set

{H} is non empty set

{{H,W0},{H}} is non empty set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

W0 is Relation-like set

H1 is Relation-like set

W0 is Relation-like set

field W0 is set

H is set

H is Relation-like set

field H is set

W0 is Relation-like set

field W0 is set

W0 is set

H1 is set

H -Seg H1 is set

Coim (H,H1) is set

{H1} is non empty set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

W0 -Seg H1 is set

Coim (W0,H1) is set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

S1 is set

H |_2 (H -Seg H1) is Relation-like set

[:(H -Seg H1),(H -Seg H1):] is Relation-like set

H /\ [:(H -Seg H1),(H -Seg H1):] is Relation-like set

field (H |_2 (H -Seg H1)) is set

W0 |_2 (W0 -Seg H1) is Relation-like set

[:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

W0 /\ [:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

field (W0 |_2 (W0 -Seg H1)) is set

H1 is set

H -Seg H1 is set

Coim (H,H1) is set

{H1} is non empty set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

S1 is set

W0 -Seg H1 is set

Coim (W0,H1) is set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

[S1,H1] is set

{S1,H1} is non empty set

{S1} is non empty set

{{S1,H1},{S1}} is non empty set

H -Seg S1 is set

Coim (H,S1) is set

(Coim (H,S1)) \ {S1} is Element of bool (Coim (H,S1))

bool (Coim (H,S1)) is non empty set

H |_2 (H -Seg H1) is Relation-like set

[:(H -Seg H1),(H -Seg H1):] is Relation-like set

H /\ [:(H -Seg H1),(H -Seg H1):] is Relation-like set

(H |_2 (H -Seg H1)) -Seg S1 is set

Coim ((H |_2 (H -Seg H1)),S1) is set

(Coim ((H |_2 (H -Seg H1)),S1)) \ {S1} is Element of bool (Coim ((H |_2 (H -Seg H1)),S1))

bool (Coim ((H |_2 (H -Seg H1)),S1)) is non empty set

W0 |_2 (W0 -Seg H1) is Relation-like set

[:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

W0 /\ [:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

(W0 |_2 (W0 -Seg H1)) -Seg S1 is set

Coim ((W0 |_2 (W0 -Seg H1)),S1) is set

(Coim ((W0 |_2 (W0 -Seg H1)),S1)) \ {S1} is Element of bool (Coim ((W0 |_2 (W0 -Seg H1)),S1))

bool (Coim ((W0 |_2 (W0 -Seg H1)),S1)) is non empty set

W0 -Seg S1 is set

Coim (W0,S1) is set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

H |_2 (H -Seg S1) is Relation-like set

[:(H -Seg S1),(H -Seg S1):] is Relation-like set

H /\ [:(H -Seg S1),(H -Seg S1):] is Relation-like set

(H |_2 (H -Seg H1)) |_2 (H -Seg S1) is Relation-like set

(H |_2 (H -Seg H1)) /\ [:(H -Seg S1),(H -Seg S1):] is Relation-like set

(W0 |_2 (W0 -Seg H1)) |_2 (W0 -Seg S1) is Relation-like set

[:(W0 -Seg S1),(W0 -Seg S1):] is Relation-like set

(W0 |_2 (W0 -Seg H1)) /\ [:(W0 -Seg S1),(W0 -Seg S1):] is Relation-like set

W0 |_2 (W0 -Seg S1) is Relation-like set

W0 /\ [:(W0 -Seg S1),(W0 -Seg S1):] is Relation-like set

H1 is set

(field H) \ W0 is Element of bool (field H)

bool (field H) is non empty set

W00 is set

W00 is set

H -Seg W00 is set

Coim (H,W00) is set

{W00} is non empty set

(Coim (H,W00)) \ {W00} is Element of bool (Coim (H,W00))

bool (Coim (H,W00)) is non empty set

a is set

[W00,a] is set

{W00,a} is non empty set

{{W00,a},{W00}} is non empty set

H -Seg a is set

Coim (H,a) is set

{a} is non empty set

(Coim (H,a)) \ {a} is Element of bool (Coim (H,a))

bool (Coim (H,a)) is non empty set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

[W00,a] is set

{W00,a} is non empty set

{{W00,a},{W00}} is non empty set

H1 is set

W0 -Seg H1 is set

Coim (W0,H1) is set

{H1} is non empty set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

S1 is set

H -Seg H1 is set

Coim (H,H1) is set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

[S1,H1] is set

{S1,H1} is non empty set

{S1} is non empty set

{{S1,H1},{S1}} is non empty set

W0 -Seg S1 is set

Coim (W0,S1) is set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

W0 |_2 (W0 -Seg H1) is Relation-like set

[:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

W0 /\ [:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

(W0 |_2 (W0 -Seg H1)) -Seg S1 is set

Coim ((W0 |_2 (W0 -Seg H1)),S1) is set

(Coim ((W0 |_2 (W0 -Seg H1)),S1)) \ {S1} is Element of bool (Coim ((W0 |_2 (W0 -Seg H1)),S1))

bool (Coim ((W0 |_2 (W0 -Seg H1)),S1)) is non empty set

H |_2 (H -Seg H1) is Relation-like set

[:(H -Seg H1),(H -Seg H1):] is Relation-like set

H /\ [:(H -Seg H1),(H -Seg H1):] is Relation-like set

(H |_2 (H -Seg H1)) -Seg S1 is set

Coim ((H |_2 (H -Seg H1)),S1) is set

(Coim ((H |_2 (H -Seg H1)),S1)) \ {S1} is Element of bool (Coim ((H |_2 (H -Seg H1)),S1))

bool (Coim ((H |_2 (H -Seg H1)),S1)) is non empty set

H -Seg S1 is set

Coim (H,S1) is set

(Coim (H,S1)) \ {S1} is Element of bool (Coim (H,S1))

bool (Coim (H,S1)) is non empty set

W0 |_2 (W0 -Seg S1) is Relation-like set

[:(W0 -Seg S1),(W0 -Seg S1):] is Relation-like set

W0 /\ [:(W0 -Seg S1),(W0 -Seg S1):] is Relation-like set

(W0 |_2 (W0 -Seg H1)) |_2 (W0 -Seg S1) is Relation-like set

(W0 |_2 (W0 -Seg H1)) /\ [:(W0 -Seg S1),(W0 -Seg S1):] is Relation-like set

(H |_2 (H -Seg H1)) |_2 (H -Seg S1) is Relation-like set

[:(H -Seg S1),(H -Seg S1):] is Relation-like set

(H |_2 (H -Seg H1)) /\ [:(H -Seg S1),(H -Seg S1):] is Relation-like set

H |_2 (H -Seg S1) is Relation-like set

H /\ [:(H -Seg S1),(H -Seg S1):] is Relation-like set

H1 is set

(field W0) \ W0 is Element of bool (field W0)

bool (field W0) is non empty set

W00 is set

W00 is set

W0 -Seg W00 is set

Coim (W0,W00) is set

{W00} is non empty set

(Coim (W0,W00)) \ {W00} is Element of bool (Coim (W0,W00))

bool (Coim (W0,W00)) is non empty set

a is set

[W00,a] is set

{W00,a} is non empty set

{{W00,a},{W00}} is non empty set

W0 -Seg a is set

Coim (W0,a) is set

{a} is non empty set

(Coim (W0,a)) \ {a} is Element of bool (Coim (W0,a))

bool (Coim (W0,a)) is non empty set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

[W00,a] is set

{W00,a} is non empty set

{{W00,a},{W00}} is non empty set

H1 is set

S1 is set

H1 is set

H -Seg H1 is set

Coim (H,H1) is set

{H1} is non empty set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

S1 is set

W00 is set

S1 is set

W0 -Seg S1 is set

Coim (W0,S1) is set

{S1} is non empty set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

N . (W0 -Seg S1) is set

H |_2 (H -Seg H1) is Relation-like set

[:(H -Seg H1),(H -Seg H1):] is Relation-like set

H /\ [:(H -Seg H1),(H -Seg H1):] is Relation-like set

W0 -Seg H1 is set

Coim (W0,H1) is set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

W0 |_2 (W0 -Seg H1) is Relation-like set

[:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

W0 /\ [:(W0 -Seg H1),(W0 -Seg H1):] is Relation-like set

W00 is set

W00 is set

a is set

[W00,a] is set

{W00,a} is non empty set

{W00} is non empty set

{{W00,a},{W00}} is non empty set

H -Seg a is set

Coim (H,a) is set

{a} is non empty set

(Coim (H,a)) \ {a} is Element of bool (Coim (H,a))

bool (Coim (H,a)) is non empty set

W0 -Seg a is set

Coim (W0,a) is set

(Coim (W0,a)) \ {a} is Element of bool (Coim (W0,a))

bool (Coim (W0,a)) is non empty set

W00 is set

a is set

[W00,a] is set

{W00,a} is non empty set

{W00} is non empty set

{{W00,a},{W00}} is non empty set

W0 -Seg a is set

Coim (W0,a) is set

{a} is non empty set

(Coim (W0,a)) \ {a} is Element of bool (Coim (W0,a))

bool (Coim (W0,a)) is non empty set

H -Seg a is set

Coim (H,a) is set

(Coim (H,a)) \ {a} is Element of bool (Coim (H,a))

bool (Coim (H,a)) is non empty set

H1 is set

S1 is set

[H1,S1] is set

{H1,S1} is non empty set

{H1} is non empty set

{{H1,S1},{H1}} is non empty set

W0 -Seg S1 is set

Coim (W0,S1) is set

{S1} is non empty set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

H -Seg S1 is set

Coim (H,S1) is set

(Coim (H,S1)) \ {S1} is Element of bool (Coim (H,S1))

bool (Coim (H,S1)) is non empty set

H1 is set

W0 -Seg H1 is set

Coim (W0,H1) is set

{H1} is non empty set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

H -Seg H1 is set

Coim (H,H1) is set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

H1 is set

S1 is set

[H1,S1] is set

{H1,S1} is non empty set

{H1} is non empty set

{{H1,S1},{H1}} is non empty set

H -Seg S1 is set

Coim (H,S1) is set

{S1} is non empty set

(Coim (H,S1)) \ {S1} is Element of bool (Coim (H,S1))

bool (Coim (H,S1)) is non empty set

W0 -Seg S1 is set

Coim (W0,S1) is set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

H1 is set

H -Seg H1 is set

Coim (H,H1) is set

{H1} is non empty set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

W0 -Seg H1 is set

Coim (W0,H1) is set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

H1 is set

H -Seg H1 is set

Coim (H,H1) is set

{H1} is non empty set

(Coim (H,H1)) \ {H1} is Element of bool (Coim (H,H1))

bool (Coim (H,H1)) is non empty set

W0 -Seg H1 is set

Coim (W0,H1) is set

(Coim (W0,H1)) \ {H1} is Element of bool (Coim (W0,H1))

bool (Coim (W0,H1)) is non empty set

S1 is set

W0 -Seg S1 is set

Coim (W0,S1) is set

{S1} is non empty set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

H -Seg S1 is set

Coim (H,S1) is set

(Coim (H,S1)) \ {S1} is Element of bool (Coim (H,S1))

bool (Coim (H,S1)) is non empty set

H is set

W0 is set

[H,W0] is set

{H,W0} is non empty set

{H} is non empty set

{{H,W0},{H}} is non empty set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

W0 is Relation-like set

H1 is Relation-like set

field W0 is set

field H1 is set

H is Relation-like set

field H is set

W0 is set

W0 is set

[W0,W0] is set

{W0,W0} is non empty set

{W0} is non empty set

{{W0,W0},{W0}} is non empty set

[W0,W0] is set

{W0,W0} is non empty set

{W0} is non empty set

{{W0,W0},{W0}} is non empty set

H1 is set

S1 is set

[H1,S1] is set

{H1,S1} is non empty set

{H1} is non empty set

{{H1,S1},{H1}} is non empty set

H1 is set

S1 is set

[H1,S1] is set

{H1,S1} is non empty set

{H1} is non empty set

{{H1,S1},{H1}} is non empty set

H is set

Z -Seg H is set

Coim (Z,H) is set

{H} is non empty set

(Coim (Z,H)) \ {H} is Element of bool (Coim (Z,H))

bool (Coim (Z,H)) is non empty set

N . (Z -Seg H) is set

W0 is Relation-like set

field W0 is set

W0 -Seg H is set

Coim (W0,H) is set

(Coim (W0,H)) \ {H} is Element of bool (Coim (W0,H))

bool (Coim (W0,H)) is non empty set

W0 is set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

W0 is set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

H1 is Relation-like set

field H1 is set

H1 -Seg H is set

Coim (H1,H) is set

(Coim (H1,H)) \ {H} is Element of bool (Coim (H1,H))

bool (Coim (H1,H)) is non empty set

H is set

W0 is set

[H,W0] is set

{H,W0} is non empty set

{H} is non empty set

{{H,W0},{H}} is non empty set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

W0 is Relation-like set

field W0 is set

H1 is Relation-like set

field H1 is set

H is set

the Element of H is Element of H

W0 is Relation-like set

field W0 is set

H /\ (field W0) is set

S1 is set

W0 -Seg S1 is set

Coim (W0,S1) is set

{S1} is non empty set

(Coim (W0,S1)) \ {S1} is Element of bool (Coim (W0,S1))

bool (Coim (W0,S1)) is non empty set

W00 is set

Z -Seg W00 is set

Coim (Z,W00) is set

{W00} is non empty set

(Coim (Z,W00)) \ {W00} is Element of bool (Coim (Z,W00))

bool (Coim (Z,W00)) is non empty set

W00 is set

[W00,W00] is set

{W00,W00} is non empty set

{W00} is non empty set

{{W00,W00},{W00}} is non empty set

a is Relation-like set

field a is set

a -Seg W00 is set

Coim (a,W00) is set

(Coim (a,W00)) \ {W00} is Element of bool (Coim (a,W00))

bool (Coim (a,W00)) is non empty set

[W00,S1] is set

{W00,S1} is non empty set

{{W00,S1},{W00}} is non empty set

W00 is set

Z -Seg W00 is set

Coim (Z,W00) is set

{W00} is non empty set

(Coim (Z,W00)) \ {W00} is Element of bool (Coim (Z,W00))

bool (Coim (Z,W00)) is non empty set

H is set

W0 is set

[H,W0] is set

{H,W0} is non empty set

{H} is non empty set

{{H,W0},{H}} is non empty set

W0 is set

[W0,W0] is set

{W0,W0} is non empty set

{W0} is non empty set

{{W0,W0},{W0}} is non empty set

[H,W0] is set

{H,W0} is non empty set

{{H,W0},{H}} is non empty set

H1 is Relation-like set

S1 is Relation-like set

W00 is Relation-like set

H1 -Seg W0 is set

Coim (H1,W0) is set

(Coim (H1,W0)) \ {W0} is Element of bool (Coim (H1,W0))

bool (Coim (H1,W0)) is non empty set

field H1 is set

field W00 is set

[W0,H] is set

{W0,H} is non empty set

{{W0,H},{W0}} is non empty set

field H1 is set

field W00 is set

W00 -Seg W0 is set

Coim (W00,W0) is set

(Coim (W00,W0)) \ {W0} is Element of bool (Coim (W00,W0))

bool (Coim (W00,W0)) is non empty set

W00 is Relation-like set

W00 is Relation-like set

field W00 is set

H is set

[H,H] is set

{H,H} is non empty set

{H} is non empty set

{{H,H},{H}} is non empty set

W0 is Relation-like set

field W0 is set

N . (field Z) is set

{(N . (field Z))} is non empty set

[:(field Z),{(N . (field Z))}:] is Relation-like set

[(N . (field Z)),(N . (field Z))] is set

{(N . (field Z)),(N . (field Z))} is non empty set

{{(N . (field Z)),(N . (field Z))},{(N . (field Z))}} is non empty set

{[(N . (field Z)),(N . (field Z))]} is non empty Relation-like Function-like set

Z \/ [:(field Z),{(N . (field Z))}:] is Relation-like set

(Z \/ [:(field Z),{(N . (field Z))}:]) \/ {[(N . (field Z)),(N . (field Z))]} is non empty Relation-like set

H1 is Relation-like set

field H1 is set

W0 is Relation-like set

field W0 is set

{(N . (field Z))} \/ {(N . (field Z))} is non empty set

(field Z) \/ {(N . (field Z))} is non empty set

W0 is Relation-like set

field W0 is set

the Element of field W0 is Element of field W0

W00 is set

[ the Element of field W0,W00] is set

{ the Element of field W0,W00} is non empty set

{ the Element of field W0} is non empty set

{{ the Element of field W0,W00},{ the Element of field W0}} is non empty set

W00 is set

[W00, the Element of field W0] is set

{W00, the Element of field W0} is non empty set

{W00} is non empty set

{{W00, the Element of field W0},{W00}} is non empty set

Z \/ W0 is Relation-like set

field (Z \/ W0) is set

(field (Z \/ W0)) \/ (field W0) is set

(field Z) \/ {} is set

((field Z) \/ {}) \/ {(N . (field Z))} is non empty set

W0 is Relation-like set

field W0 is set

Z \/ W0 is Relation-like set

field (Z \/ W0) is set

(field (Z \/ W0)) \/ (field W0) is set

(field Z) \/ ((field Z) \/ {(N . (field Z))}) is non empty set

((field Z) \/ ((field Z) \/ {(N . (field Z))})) \/ {(N . (field Z))} is non empty set

(field Z) \/ (field Z) is set

((field Z) \/ (field Z)) \/ {(N . (field Z))} is non empty set

(((field Z) \/ (field Z)) \/ {(N . (field Z))}) \/ {(N . (field Z))} is non empty set

((field Z) \/ (field Z)) \/ ({(N . (field Z))} \/ {(N . (field Z))}) is non empty set

S1 is set

W0 is Relation-like set

S1 is set

W00 is set

[S1,W00] is set

{S1,W00} is non empty set

{S1} is non empty set

{{S1,W00},{S1}} is non empty set

Z \/ W0 is Relation-like set

S1 is set

W00 is set

[S1,W00] is set

{S1,W00} is non empty set

{S1} is non empty set

{{S1,W00},{S1}} is non empty set

[W00,S1] is set

{W00,S1} is non empty set

{W00} is non empty set

{{W00,S1},{W00}} is non empty set

S1 is set

W00 is set

[S1,W00] is set

{S1,W00} is non empty set

{S1} is non empty set

{{S1,W00},{S1}} is non empty set

S1 is set

W00 is set

[S1,W00] is set

{S1,W00} is non empty set

{S1} is non empty set

{{S1,W00},{S1}} is non empty set

S1 is set

W00 is set

[S1,W00] is set

{S1,W00} is non empty set

{S1} is non empty set

{{S1,W00},{S1}} is non empty set

[W00,S1] is set

{W00,S1} is non empty set

{W00} is non empty set

{{W00,S1},{W00}} is non empty set

S1 is set

H1 -Seg S1 is set

Coim (H1,S1) is set

{S1} is non empty set

(Coim (H1,S1)) \ {S1} is Element of bool (Coim (H1,S1))

bool (Coim (H1,S1)) is non empty set

Z -Seg S1 is set

Coim (Z,S1) is set

(Coim (Z,S1)) \ {S1} is Element of bool (Coim (Z,S1))

bool (Coim (Z,S1)) is non empty set

W00 is set

[W00,S1] is set

{W00,S1} is non empty set

{W00} is non empty set

{{W00,S1},{W00}} is non empty set

W00 is set

[W00,S1] is set

{W00,S1} is non empty set

{W00} is non empty set

{{W00,S1},{W00}} is non empty set

S1 is set

(field Z) /\ S1 is set

W00 is set

Z -Seg W00 is set

Coim (Z,W00) is set

{W00} is non empty set

(Coim (Z,W00)) \ {W00} is Element of bool (Coim (Z,W00))

bool (Coim (Z,W00)) is non empty set

(Z -Seg W00) /\ S1 is set

(Z -Seg W00) /\ ((field Z) /\ S1) is set

a is set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

H1 -Seg W00 is set

Coim (H1,W00) is set

(Coim (H1,W00)) \ {W00} is Element of bool (Coim (H1,W00))

bool (Coim (H1,W00)) is non empty set

(H1 -Seg W00) /\ S1 is set

the Element of S1 is Element of S1

H1 -Seg (N . (field Z)) is set

Coim (H1,(N . (field Z))) is set

(Coim (H1,(N . (field Z)))) \ {(N . (field Z))} is Element of bool (Coim (H1,(N . (field Z))))

bool (Coim (H1,(N . (field Z)))) is non empty set

W00 is set

[W00,(N . (field Z))] is set

{W00,(N . (field Z))} is non empty set

{W00} is non empty set

{{W00,(N . (field Z))},{W00}} is non empty set

H1 -Seg the Element of S1 is set

Coim (H1, the Element of S1) is set

{ the Element of S1} is non empty set

(Coim (H1, the Element of S1)) \ { the Element of S1} is Element of bool (Coim (H1, the Element of S1))

bool (Coim (H1, the Element of S1)) is non empty set

(H1 -Seg the Element of S1) /\ S1 is set

W00 is set

H1 -Seg W00 is set

Coim (H1,W00) is set

{W00} is non empty set

(Coim (H1,W00)) \ {W00} is Element of bool (Coim (H1,W00))

bool (Coim (H1,W00)) is non empty set

W00 is set

H1 -Seg W00 is set

Coim (H1,W00) is set

{W00} is non empty set

(Coim (H1,W00)) \ {W00} is Element of bool (Coim (H1,W00))

bool (Coim (H1,W00)) is non empty set

W00 is set

Z -Seg W00 is set

Coim (Z,W00) is set

{W00} is non empty set

(Coim (Z,W00)) \ {W00} is Element of bool (Coim (Z,W00))

bool (Coim (Z,W00)) is non empty set

H1 -Seg W00 is set

Coim (H1,W00) is set

(Coim (H1,W00)) \ {W00} is Element of bool (Coim (H1,W00))

bool (Coim (H1,W00)) is non empty set

W00 is set

H1 -Seg W00 is set

Coim (H1,W00) is set

{W00} is non empty set

(Coim (H1,W00)) \ {W00} is Element of bool (Coim (H1,W00))

bool (Coim (H1,W00)) is non empty set

W00 is set

H1 -Seg W00 is set

Coim (H1,W00) is set

{W00} is non empty set

(Coim (H1,W00)) \ {W00} is Element of bool (Coim (H1,W00))

bool (Coim (H1,W00)) is non empty set

S1 is set

H1 -Seg S1 is set

Coim (H1,S1) is set

{S1} is non empty set

(Coim (H1,S1)) \ {S1} is Element of bool (Coim (H1,S1))

bool (Coim (H1,S1)) is non empty set

N . (H1 -Seg S1) is set

Z -Seg S1 is set

Coim (Z,S1) is set

(Coim (Z,S1)) \ {S1} is Element of bool (Coim (Z,S1))

bool (Coim (Z,S1)) is non empty set

W00 is set

[W00,S1] is set

{W00,S1} is non empty set

{W00} is non empty set

{{W00,S1},{W00}} is non empty set

Z \/ W0 is Relation-like set

W00 is set

[W00,S1] is set

{W00,S1} is non empty set

{W00} is non empty set

{{W00,S1},{W00}} is non empty set

Z \/ W0 is Relation-like set

H1 -Seg (N . (field Z)) is set

Coim (H1,(N . (field Z))) is set

(Coim (H1,(N . (field Z)))) \ {(N . (field Z))} is Element of bool (Coim (H1,(N . (field Z))))

bool (Coim (H1,(N . (field Z)))) is non empty set

W00 is set

[W00,(N . (field Z))] is set

{W00,(N . (field Z))} is non empty set

{W00} is non empty set

{{W00,(N . (field Z))},{W00}} is non empty set

W00 is set

[W00,(N . (field Z))] is set

{W00,(N . (field Z))} is non empty set

{W00} is non empty set

{{W00,(N . (field Z))},{W00}} is non empty set

Z \/ W0 is Relation-like set

S1 is set

W00 is set

[S1,W00] is set

{S1,W00} is non empty set

{S1} is non empty set

{{S1,W00},{S1}} is non empty set

W00 is set

[W00,W00] is set

{W00,W00} is non empty set

{W00} is non empty set

{{W00,W00},{W00}} is non empty set

[S1,W00] is set

{S1,W00} is non empty set

{{S1,W00},{S1}} is non empty set

S1 is set

[S1,S1] is set

{S1,S1} is non empty set

{S1} is non empty set

{{S1,S1},{S1}} is non empty set

H is set

Z -Seg H is set

Coim (Z,H) is set

{H} is non empty set

(Coim (Z,H)) \ {H} is Element of bool (Coim (Z,H))

bool (Coim (Z,H)) is non empty set

N . (Z -Seg H) is set

N is set

M is set

D is set

D is set

D is set

F is set

N is set

M is set

bool M is non empty set

D is set

union D is set

F is set

S is set

id D is Relation-like D -defined D -valued Function-like one-to-one set

S is set

(id D) . S is set

Z is set

{Z} is non empty set

bool Z is non empty set

H is set

W0 is set

[W0,(bool Z)] is set

{W0,(bool Z)} is non empty set

{W0} is non empty set

{{W0,(bool Z)},{W0}} is non empty set

W0 is set

[W0,Z] is set

{W0,Z} is non empty set

{W0} is non empty set

{{W0,Z},{W0}} is non empty set

H is set

S is Relation-like set

field S is set

Z is set

H is set

W0 is set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

H is set

W0 is set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

W0 is set

[W0,H] is set

{W0,H} is non empty set

{W0} is non empty set

{{W0,H},{W0}} is non empty set

H is Relation-like Function-like set

dom H is set

[:M,M:] is Relation-like set

W0 is set

rng H is set

W0 is set

H1 is set

[W0,H1] is set

{W0,H1} is non empty set

{W0} is non empty set

{{W0,H1},{W0}} is non empty set

H . H1 is set

[(H . H1),H1] is set

{(H . H1),H1} is non empty set

{(H . H1)} is non empty set

{{(H . H1),H1},{(H . H1)}} is non empty set

W0 is set

H . W0 is set

H1 is set

H . H1 is set

[(H . W0),W0] is set

{(H . W0),W0} is non empty set

{(H . W0)} is non empty set

{{(H . W0),W0},{(H . W0)}} is non empty set

[(H . H1),H1] is set

{(H . H1),H1} is non empty set

{(H . H1)} is non empty set

{{(H . H1),H1},{(H . H1)}} is non empty set

W0 is set

H1 is set

S1 is set

[H1,S1] is set

{H1,S1} is non empty set

{H1} is non empty set

{{H1,S1},{H1}} is non empty set

H . H1 is set

H . S1 is set

[(H . H1),(H . S1)] is set

{(H . H1),(H . S1)} is non empty set

{(H . H1)} is non empty set

{{(H . H1),(H . S1)},{(H . H1)}} is non empty set

W0 is Relation-like set

field W0 is set

H1 is set

S1 is set

[H1,S1] is set

{H1,S1} is non empty set

{H1} is non empty set

{{H1,S1},{H1}} is non empty set

[S1,H1] is set

{S1,H1} is non empty set

{S1} is non empty set

{{S1,H1},{S1}} is non empty set

H1 is set

{H1} is non empty set

H1 is set

S1 is set

{H1} is non empty set

W00 is set

H1 is Relation-like Function-like set

dom H1 is set

S1 is set

H1 . S1 is set

W00 is set

H1 . W00 is set

{S1} is non empty set

{W00} is non empty set

rng H1 is set

W0 |_2 (rng H1) is Relation-like set

[:(rng H1),(rng H1):] is Relation-like set

W0 /\ [:(rng H1),(rng H1):] is Relation-like set

W00 is set

W00 is set

H . W00 is set

[W00,W00] is set

{W00,W00} is non empty set

{W00} is non empty set

{{W00,W00},{W00}} is non empty set

a is set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

W00 is set

H . W00 is set

W00 is set

[(H . W00),W00] is set

{(H . W00),W00} is non empty set

{(H . W00)} is non empty set

{{(H . W00),W00},{(H . W00)}} is non empty set

[W00,(H . W00)] is set

{W00,(H . W00)} is non empty set

{W00} is non empty set

{{W00,(H . W00)},{W00}} is non empty set

a is set

H . a is set

[W00,a] is set

{W00,a} is non empty set

{W00} is non empty set

{{W00,a},{W00}} is non empty set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

a is set

H . a is set

[W00,a] is set

{W00,a} is non empty set

{W00} is non empty set

{{W00,a},{W00}} is non empty set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

a is set

[W00,a] is set

{W00,a} is non empty set

{W00} is non empty set

{{W00,a},{W00}} is non empty set

b is set

[b,W00] is set

{b,W00} is non empty set

{b} is non empty set

{{b,W00},{b}} is non empty set

x is set

[W00,x] is set

{W00,x} is non empty set

{{W00,x},{W00}} is non empty set

y is set

[y,W00] is set

{y,W00} is non empty set

{y} is non empty set

{{y,W00},{y}} is non empty set

W00 is set

[W00,W00] is set

{W00,W00} is non empty set

{W00} is non empty set

{{W00,W00},{W00}} is non empty set

a is set

[a,W00] is set

{a,W00} is non empty set

{a} is non empty set

{{a,W00},{a}} is non empty set

W00 is set

H . W00 is set

W00 is set

[W00,W00] is set

{W00,W00} is non empty set

{W00} is non empty set

{{W00,W00},{W00}} is non empty set

H . W00 is set

[(H . W00),(H . W00)] is set

{(H . W00),(H . W00)} is non empty set

{(H . W00)} is non empty set

{{(H . W00),(H . W00)},{(H . W00)}} is non empty set

a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

H . a is set

H . b is set

[(H . a),(H . b)] is set

{(H . a),(H . b)} is non empty set

{(H . a)} is non empty set

{{(H . a),(H . b)},{(H . a)}} is non empty set

H " is Relation-like Function-like set

[:N,N:] is Relation-like set

W00 is set

W00 is set

a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

H1 . a is set

H1 . b is set

[(H1 . a),(H1 . b)] is set

{(H1 . a),(H1 . b)} is non empty set

{(H1 . a)} is non empty set

{{(H1 . a),(H1 . b)},{(H1 . a)}} is non empty set

W00 is Relation-like set

field W00 is set

a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

[b,a] is set

{b,a} is non empty set

{b} is non empty set

{{b,a},{b}} is non empty set

a is set

b is set

H1 . b is set

{b} is non empty set

x is set

field (W0 |_2 (rng H1)) is set

a is set

H1 . a is set

b is set

[(H1 . a),b] is set

{(H1 . a),b} is non empty set

{(H1 . a)} is non empty set

{{(H1 . a),b},{(H1 . a)}} is non empty set

[b,(H1 . a)] is set

{b,(H1 . a)} is non empty set

{b} is non empty set

{{b,(H1 . a)},{b}} is non empty set

x is set

H1 . x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

x is set

H1 . x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

y is set

[y,a] is set

{y,a} is non empty set

{y} is non empty set

{{y,a},{y}} is non empty set

c

[a,c

{a,c

{{a,c

c

[c

{c

{c

{{c

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

x is set

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

a is set

H1 . a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

H1 . b is set

[(H1 . a),(H1 . b)] is set

{(H1 . a),(H1 . b)} is non empty set

{(H1 . a)} is non empty set

{{(H1 . a),(H1 . b)},{(H1 . a)}} is non empty set

x is set

y is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

H1 . x is set

H1 . y is set

[(H1 . x),(H1 . y)] is set

{(H1 . x),(H1 . y)} is non empty set

{(H1 . x)} is non empty set

{{(H1 . x),(H1 . y)},{(H1 . x)}} is non empty set

H1 " is Relation-like Function-like set