:: 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₁ "\/" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in a & b₂ in X ) } is set
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₁} "/\" (proj2 a)),H)) where b₁ is Element of the carrier of H : b₁ in proj1 a } is set
{ ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
{ ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
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₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
(proj1 a) "/\" (proj2 a) is Element of bool the carrier of H
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in proj1 a & b₂ in proj2 a ) } is set
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
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₁) where b₁ is Element of the carrier of H : b₁ in proj2 a } is set
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₁) where b₁ is Element of the carrier of H : b₁ in proj2 a } is set
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₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } 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
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" X1 & b₂ in X ) } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" X1 & b₂ in X ) } is set
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₁,H)) where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } 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
{ ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
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₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
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₁) where b₁ is Element of the carrier of H : b₁ in X1 } is set
"\/" (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₁,H)) where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
"\/" ( { ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } ,H) is Element of the carrier of H
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
"\/" ((union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } ),H) is Element of the carrier of H
{ ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
"\/" ((union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } ),H) is Element of the carrier of H
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₁,H)) where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
"\/" ( { ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } ,H) is Element of the carrier of H
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } is set
"\/" ((union { b₁ where b₁ is non empty directed Element of bool the carrier of H : ex b₂ being Element of the carrier of H st
( b₁ = {b₂} "/\" (proj2 a) & b₂ in proj1 a ) } ),H) is Element of the carrier of H
{ ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
"\/" ( { ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } ,H) is Element of the carrier of H
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
"\/" ((union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } ),H) is Element of the carrier of H
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₁) where b₁ is Element of the carrier of H : b₁ in X } is set
"\/" ( { (a "/\" b₁) where b₁ is Element of the carrier of H : b₁ in X } ,H) is Element of the carrier of H
{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₁() is non empty RelStr
the carrier of F₁() is non empty set
F₂() is non empty directed NetStr over F₁()
the carrier of F₂() is non empty set
the InternalRel of F₂() is Relation-like the carrier of F₂() -defined the carrier of F₂() -valued Element of bool [: the carrier of F₂(), the carrier of F₂():]
[: the carrier of F₂(), the carrier of F₂():] is non empty Relation-like set
bool [: the carrier of F₂(), the carrier of F₂():] is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of F₂(), the InternalRel of F₂() #) is non empty strict RelStr
the mapping of F₂() is non empty Relation-like the carrier of F₂() -defined the carrier of F₁() -valued Function-like V31( the carrier of F₂()) V33( the carrier of F₂(), the carrier of F₁()) Element of bool [: the carrier of F₂(), the carrier of F₁():]
[: the carrier of F₂(), the carrier of F₁():] is non empty Relation-like set
bool [: the carrier of F₂(), the carrier of F₁():] is non empty cup-closed diff-closed preBoolean set
H is Element of the carrier of F₂()
the mapping of F₂() . H is Element of the carrier of F₁()
F₃(( the mapping of F₂() . H)) is Element of the carrier of F₁()
H is non empty Relation-like the carrier of F₂() -defined the carrier of F₁() -valued Function-like V31( the carrier of F₂()) V33( the carrier of F₂(), the carrier of F₁()) Element of bool [: the carrier of F₂(), the carrier of F₁():]
NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) is non empty strict NetStr over F₁()
the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) is non empty set
the InternalRel of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) is Relation-like the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) -defined the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) -valued Element of bool [: the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #), the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #):]
[: the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #), the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #):] is non empty Relation-like set
bool [: the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #), the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #):] is non empty cup-closed diff-closed preBoolean set
RelStr(# the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #), the InternalRel of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) #) is non empty strict RelStr
[#] F₂() is non empty non proper lower upper Element of bool the carrier of F₂()
bool the carrier of F₂() is non empty cup-closed diff-closed preBoolean set
[#] NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) is non empty non proper lower upper Element of bool the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #)
bool the carrier of NetStr(# the carrier of F₂(), the InternalRel of F₂(),H #) is non empty cup-closed diff-closed preBoolean set
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₁() -valued Function-like V31( the carrier of X) V33( the carrier of X, the carrier of F₁()) Element of bool [: the carrier of X, the carrier of F₁():]
[: the carrier of X, the carrier of F₁():] is non empty Relation-like set
bool [: the carrier of X, the carrier of F₁():] is non empty cup-closed diff-closed preBoolean set
X1 is Element of the carrier of X
the mapping of X . X1 is Element of the carrier of F₁()
the mapping of F₂() . X1 is set
F₃(( the mapping of F₂() . X1)) is Element of the carrier of 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₁) where b₁ is Element of the carrier of H : b₁ in rng the mapping of 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 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)
bool the carrier of (H,a,X) is non empty cup-closed diff-closed preBoolean set
dom the mapping of X is non empty Element of bool the carrier of X
bool the carrier of X is non empty cup-closed diff-closed preBoolean set
h is set
a is set
the mapping of (H,a,X) . a is set
y is Element of the carrier of (H,a,X)
the mapping of X . y is set
the mapping of (H,a,X) . y is Element of the carrier of H
Y is Element of the carrier of H
a "/\" Y is Element of the carrier of H
h is set
a is Element of the carrier of H
a "/\" a is Element of the carrier of H
y is set
the mapping of X . y is set
Y is Element of the carrier of (H,a,X)
the mapping of X . Y is set
the mapping of (H,a,X) . 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 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
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) 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
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:]
rng (netmap ((H,a,X),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
rng X is Element of bool the carrier of H
finsups (rng X) is Element of bool the carrier of H
bool (rng X) is non empty cup-closed diff-closed preBoolean set
{ ("\/" (b₁,H)) where b₁ is finite Element of bool (rng X) : ex_sup_of b₁,H } is set
X1 is set
dom (netmap ((H,a,X),H)) is non empty 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
f is set
(netmap ((H,a,X),H)) . f 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
a 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)),a #) is non empty strict NetStr over H
h is finite Element of Fin a
X .: h is finite Element of bool the carrier of H
(netmap ((H,a,X),H)) . h is set
"\/" ((X .: h),H) is Element of the carrier of H
a 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)),a #) is non empty strict NetStr over H
H is non empty V70() reflexive antisymmetric non void 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 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:]
rng X is Element of bool the carrier of H
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
(H,a,X) is non empty directed NetStr over H
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) 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
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:]
rng (netmap ((H,a,X),H)) is non empty Element of bool the carrier of H
X1 is set
dom X is Element of bool a
bool a is non empty cup-closed diff-closed preBoolean set
xx is set
X . xx is set
f is Element of a
X . f is set
Im (X,f) is set
{f} is non empty trivial finite V53(1) set
X .: {f} is finite set
h is Element of the carrier of H
{h} is non empty trivial finite V53(1) Element of bool the carrier of H
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
y 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)),y #) is non empty strict NetStr over H
dom y is non empty Element of bool (Fin a)
bool (Fin a) is non empty cup-closed diff-closed preBoolean set
a is finite Element of Fin a
y . {f} is set
X .: a is finite Element of bool the carrier of H
"\/" ((X .: a),H) is Element of the carrier of H
H is non empty V70() reflexive antisymmetric non void 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
Fin a 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:]
rng X is Element of bool the carrier of H
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
(H,a,X) is non empty directed NetStr over H
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) 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
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:]
rng (netmap ((H,a,X),H)) is non empty Element of bool the carrier of H
\\/ (X,H) is Element of the carrier of H
(H,(H,a,X)) is Element of the carrier of H
\\/ ( the mapping of (H,a,X),H) is Element of the carrier of H
"\/" ((rng X),H) is Element of the carrier of H
"\/" ((rng (netmap ((H,a,X),H))),H) is Element of the carrier of H
xx is Element of the carrier of H
dom (netmap ((H,a,X),H)) is non empty 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
f is set
(netmap ((H,a,X),H)) . f is 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
a 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)),a #) is non empty strict NetStr over H
h is finite Element of Fin a
X .: h is finite Element of bool the carrier of H
"\/" ((X .: h),H) is Element of the carrier of H
a 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)),a #) is non empty strict NetStr over H
H is non empty transitive antisymmetric with_infima RelStr
the carrier of H is non empty set
a is non empty directed NetStr over H
X is Element of the carrier of H
(H,X,a) is non empty strict directed NetStr over H
the carrier of (H,X,a) is non empty 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 non empty 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 non empty strict RelStr
the carrier of a is non empty set
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
X1 is Element of the carrier of (H,X,a)
(H,X,a) . X1 is Element of the carrier of H
the mapping of (H,X,a) is non empty Relation-like the carrier of (H,X,a) -defined the carrier of H -valued Function-like V31( the carrier of (H,X,a)) V33( the carrier of (H,X,a), the carrier of H) Element of bool [: the carrier of (H,X,a), the carrier of H:]
[: the carrier of (H,X,a), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (H,X,a), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
the mapping of (H,X,a) . X1 is Element of the carrier of H
xx is Element of the carrier of a
a . xx is Element of the carrier of H
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:]
[: 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 . xx is Element of the carrier of H
f is Element of the carrier of a
h is Element of the carrier of (H,X,a)
a is Element of the carrier of (H,X,a)
(H,X,a) . a is Element of the carrier of H
the mapping of (H,X,a) . a is Element of the carrier of H
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
the mapping of a . X1 is set
the mapping of a . a is set
Y is Element of the carrier of H
X "/\" Y is Element of the carrier of H
z is Element of the carrier of H
X "/\" z is Element of the carrier of H
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
"\/" (a,H) is Element of the carrier of H
X is Element of the carrier of H
X "/\" ("\/" (a,H)) 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
"\/" (({X} "/\" a),H) is Element of the carrier of H
X1 is Element of the carrier of H
{(X "/\" ("\/" (a,H)))} is non empty trivial finite V53(1) Element of bool the carrier of H
{(X "/\" ("\/" (a,H)))} "/\" a is non empty Element of bool the carrier of H
"\/" (({(X "/\" ("\/" (a,H)))} "/\" a),H) is Element of 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
{("\/" (a,H))} is non empty trivial finite V53(1) Element of bool the carrier of H
{X} "/\" {("\/" (a,H))} is non empty Element of bool the carrier of H
({X} "/\" {("\/" (a,H))}) "/\" a is non empty Element of bool the carrier of H
"\/" ((({X} "/\" {("\/" (a,H))}) "/\" a),H) is Element of the carrier of H
{("\/" (a,H))} "/\" a is non empty Element of bool the carrier of H
{X} "/\" ({("\/" (a,H))} "/\" a) is non empty Element of bool the carrier of H
"\/" (({X} "/\" ({("\/" (a,H))} "/\" a)),H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric 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 Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
finsups a is directed Element of bool the carrier of H
bool a is non empty cup-closed diff-closed preBoolean set
{ ("\/" (b₁,H)) where b₁ is finite Element of bool a : ex_sup_of b₁,H } is set
X is Element of the carrier of H
X "/\" ("\/" (a,H)) is Element of the carrier of H
{X} is non empty trivial finite V53(1) Element of bool the carrier of H
{X} "/\" (finsups a) is Element of bool the carrier of H
"\/" (({X} "/\" (finsups a)),H) is Element of the carrier of H
"\/" ((finsups a),H) is Element of the carrier of H
X "/\" ("\/" ((finsups a),H)) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema 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
"\/" (a,H) is Element of the carrier of H
X is Element of the carrier of H
X "/\" ("\/" (a,H)) 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
"\/" (({X} "/\" a),H) is Element of 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
finsups a is non empty directed Element of bool the carrier of H
bool a is non empty cup-closed diff-closed preBoolean set
{ ("\/" (b₁,H)) where b₁ is finite Element of bool a : ex_sup_of b₁,H } is set
{X} "/\" (finsups a) is non empty Element of bool the carrier of H
{ (X "/\" b₁) where b₁ is Element of the carrier of H : b₁ in finsups a } is set
xx is Element of the carrier of H
f is Element of the carrier of H
X "/\" f is Element of the carrier of H
h is finite Element of bool a
"\/" (h,H) is Element of the carrier of H
a is Element of the carrier of H
X "/\" a is Element of the carrier of H
X1 "/\" (finsups a) is non empty directed Element of bool the carrier of H
"\/" (({X} "/\" (finsups a)),H) is Element of the carrier of H
H is non empty RelStr
[:H,H:] is non empty strict RelStr
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean 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
a is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
X is Element of the carrier of H
X1 is Element of the carrier of H
a . (X,X1) is set
[X,X1] is V1() set
{X,X1} is non empty finite set
{X} is non empty trivial finite V53(1) set
{{X,X1},{X}} is non empty finite V50() set
a . [X,X1] is set
X "/\" X1 is Element of the carrier of H
a is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
X is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
X1 is Element of the carrier of H
xx is Element of the carrier of H
a . (X1,xx) is set
[X1,xx] is V1() set
{X1,xx} is non empty finite set
{X1} is non empty trivial finite V53(1) set
{{X1,xx},{X1}} is non empty finite V50() set
a . [X1,xx] is set
X1 "/\" xx is Element of the carrier of H
X . (X1,xx) is set
X . [X1,xx] is set
H is non empty RelStr
[:H,H:] is non empty strict RelStr
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of [:H,H:]
(H) . a is Element of the carrier of H
a `1 is Element of the carrier of H
a `2 is Element of the carrier of H
(a `1) "/\" (a `2) is Element of the carrier of H
[: the carrier of H, the carrier of H:] is non empty Relation-like set
(H) . ((a `1),(a `2)) is set
[(a `1),(a `2)] is V1() set
{(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) . [(a `1),(a `2)] is set
X is set
X1 is set
[X,X1] is V1() set
{X,X1} is non empty finite set
{X} is non empty trivial finite V53(1) set
{{X,X1},{X}} is non empty finite V50() set
H is non empty transitive antisymmetric with_infima RelStr
[:H,H:] is non empty strict transitive antisymmetric with_infima RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of [:H,H:]
X is Element of the carrier of [:H,H:]
(H) . a is set
(H) . X is set
a `1 is Element of the carrier of H
X `1 is Element of the carrier of H
a `2 is Element of the carrier of H
X `2 is Element of the carrier of H
(H) . a is Element of the carrier of H
(a `1) "/\" (a `2) is Element of the carrier of H
(H) . X is Element of the carrier of H
(X `1) "/\" (X `2) is Element of the carrier of H
xx is Element of the carrier of H
f is Element of the carrier of H
H is non empty RelStr
the carrier of H is non empty set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
[:H,H:] is non empty strict RelStr
the carrier of [:H,H:] is non empty set
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of bool the carrier of H
X is Element of bool the carrier of H
[:a,X:] is Relation-like Element of bool the carrier of [:H,H:]
bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set
(H) .: [:a,X:] is Element of bool the carrier of H
a "/\" X is Element of bool the carrier of H
f is set
h is Element of the carrier of H
a is Element of the carrier of [:H,H:]
(H) . a is Element of the carrier of H
y is set
Y is set
[y,Y] is V1() set
{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
z is Element of the carrier of H
y is Element of the carrier of H
(H) . (z,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
(H) . [z,y] is set
z "/\" y is Element of the carrier of H
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in a & b₂ in X ) } is set
f is set
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in a & b₂ in X ) } 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) . (h,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
(H) . [h,a] is set
[h,a] is V1() Element of the carrier of [:H,H:]
xx is set
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 up-complete 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
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,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,H:]
(H) .: a is non empty Element of bool the carrier of H
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
"\/" (((H) .: a),H) is Element of the carrier of H
proj1 a is Element of bool the carrier of H
proj2 a is Element of bool the carrier of H
(proj1 a) "/\" (proj2 a) is Element of bool the carrier of H
"\/" (((proj1 a) "/\" (proj2 a)),H) is Element of the carrier of H
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty cup-closed diff-closed preBoolean set
xx is non empty directed Element of bool the carrier of H
f is non empty directed Element of bool the carrier of H
xx "/\" f is non empty directed Element of bool the carrier of H
[:xx,f:] is non empty Relation-like directed Element of bool the carrier of [:H,H:]
(H) .: [:xx,f:] is non empty Element of bool the carrier of H
downarrow a is non empty directed lower Element of bool the carrier of [:H,H:]
(H) .: (downarrow a) is non empty Element of bool the carrier of H
downarrow ((H) .: a) is non empty lower Element of bool the carrier of H
"\/" ((xx "/\" f),H) is Element of the carrier of H
"\/" ((downarrow ((H) .: a)),H) is Element of the carrier of H
X1 is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
(H) .: X1 is Element of bool the carrier of H
H is non empty RelStr
[:H,H:] is non empty strict RelStr
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean 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
a is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
X is Element of the carrier of H
X1 is Element of the carrier of H
a . (X,X1) is set
[X,X1] is V1() set
{X,X1} is non empty finite set
{X} is non empty trivial finite V53(1) set
{{X,X1},{X}} is non empty finite V50() set
a . [X,X1] is set
X "\/" X1 is Element of the carrier of H
a is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
X is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
X1 is Element of the carrier of H
xx is Element of the carrier of H
a . (X1,xx) is set
[X1,xx] is V1() set
{X1,xx} is non empty finite set
{X1} is non empty trivial finite V53(1) set
{{X1,xx},{X1}} is non empty finite V50() set
a . [X1,xx] is set
X1 "\/" xx is Element of the carrier of H
X . (X1,xx) is set
X . [X1,xx] is set
H is non empty RelStr
[:H,H:] is non empty strict RelStr
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of [:H,H:]
(H) . a is Element of the carrier of H
a `1 is Element of the carrier of H
a `2 is Element of the carrier of H
(a `1) "\/" (a `2) is Element of the carrier of H
[: the carrier of H, the carrier of H:] is non empty Relation-like set
(H) . ((a `1),(a `2)) is set
[(a `1),(a `2)] is V1() set
{(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) . [(a `1),(a `2)] is set
X is set
X1 is set
[X,X1] is V1() set
{X,X1} is non empty finite set
{X} is non empty trivial finite V53(1) set
{{X,X1},{X}} is non empty finite V50() set
H is non empty transitive antisymmetric with_suprema RelStr
[:H,H:] is non empty strict transitive antisymmetric with_suprema RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of [:H,H:]
X is Element of the carrier of [:H,H:]
(H) . a is set
(H) . X is set
a `1 is Element of the carrier of H
X `1 is Element of the carrier of H
a `2 is Element of the carrier of H
X `2 is Element of the carrier of H
(H) . a is Element of the carrier of H
(a `1) "\/" (a `2) is Element of the carrier of H
(H) . X is Element of the carrier of H
(X `1) "\/" (X `2) is Element of the carrier of H
xx is Element of the carrier of H
f is Element of the carrier of H
H is non empty RelStr
the carrier of H is non empty set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
[:H,H:] is non empty strict RelStr
the carrier of [:H,H:] is non empty set
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of bool the carrier of H
X is Element of bool the carrier of H
[:a,X:] is Relation-like Element of bool the carrier of [:H,H:]
bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set
(H) .: [:a,X:] is Element of bool the carrier of H
a "\/" X is Element of bool the carrier of H
f is set
h is Element of the carrier of H
a is Element of the carrier of [:H,H:]
(H) . a is Element of the carrier of H
y is set
Y is set
[y,Y] is V1() set
{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
z is Element of the carrier of H
y is Element of the carrier of H
(H) . (z,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
(H) . [z,y] is set
z "\/" y is Element of the carrier of H
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in a & b₂ in X ) } is set
f is set
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in a & b₂ in X ) } 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) . (h,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
(H) . [h,a] is set
[h,a] is V1() Element of the carrier of [:H,H:]
xx is set
H is non empty V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:H,H:] is non empty strict V70() reflexive transitive antisymmetric lower-bounded upper-bounded V134() up-complete /\-complete non void with_suprema with_infima complete 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
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is non empty filtered Element of bool the carrier of [:H,H:]
(H) .: a is non empty Element of bool the carrier of H
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
"/\" (((H) .: a),H) is Element of the carrier of H
proj1 a is Element of bool the carrier of H
proj2 a is Element of bool the carrier of H
(proj1 a) "\/" (proj2 a) is Element of bool the carrier of H
"/\" (((proj1 a) "\/" (proj2 a)),H) is Element of the carrier of H
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty cup-closed diff-closed preBoolean set
uparrow ((H) .: a) is non empty upper Element of bool the carrier of H
[:(proj1 a),(proj2 a):] is Relation-like Element of bool the carrier of [:H,H:]
(H) .: [:(proj1 a),(proj2 a):] is Element of bool the carrier of H
uparrow a is non empty filtered upper Element of bool the carrier of [:H,H:]
(H) .: (uparrow a) is non empty Element of bool the carrier of H
"/\" ((uparrow ((H) .: a)),H) is Element of the carrier of H
X1 is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
(H) .: X1 is Element of bool the carrier of H
H is non empty trivial finite 1 -element 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
the carrier of H is non empty trivial finite V53(1) set
bool the carrier of H is non empty cup-closed diff-closed preBoolean finite V50() 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 non empty trivial finite V53(1) directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
a "/\" ("\/" (X,H)) is Element of the carrier of H
{a} "/\" X is non empty trivial finite V53(1) Element of bool the carrier of H
"\/" (({a} "/\" X),H) is Element of the carrier of H
H is non empty V70() reflexive non void RelStr
H is non empty V70() reflexive non void RelStr
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
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 non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
a "/\" ("\/" (X,H)) is Element of the carrier of H
{a} "/\" X is non empty Element of bool the carrier of H
"\/" (({a} "/\" X),H) is Element of the carrier of H
{ (a "/\" b₁) where b₁ is Element of the carrier of H : b₁ in X } is set
"\/" ( { (a "/\" b₁) where b₁ is Element of the carrier of H : b₁ in X } ,H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr
Ids H is non empty set
the carrier of H is non empty set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of H : verum } is set
InclPoset (Ids H) is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr
SupMap H is non empty Relation-like the carrier of (InclPoset (Ids H)) -defined the carrier of H -valued Function-like V31( the carrier of (InclPoset (Ids H))) V33( the carrier of (InclPoset (Ids H)), the carrier of H) monotone Element of bool [: the carrier of (InclPoset (Ids H)), the carrier of H:]
the carrier of (InclPoset (Ids H)) is non empty set
[: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
X is non empty directed lower Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
X1 is non empty directed lower Element of bool the carrier of H
"\/" (X1,H) is Element of the carrier of H
("\/" (X,H)) "/\" ("\/" (X1,H)) is Element of the carrier of H
X "/\" X1 is non empty directed lower Element of bool the carrier of H
"\/" ((X "/\" X1),H) is Element of the carrier of H
xx is Element of the carrier of (InclPoset (Ids H))
f is Element of the carrier of (InclPoset (Ids H))
{xx,f} is non empty finite Element of bool the carrier of (InclPoset (Ids H))
bool the carrier of (InclPoset (Ids H)) is non empty cup-closed diff-closed preBoolean set
(SupMap H) . xx is Element of the carrier of H
h is Element of the carrier of H
h "/\" ("\/" (X1,H)) is Element of the carrier of H
(SupMap H) . f is Element of the carrier of H
((SupMap H) . xx) "/\" ((SupMap H) . f) is Element of the carrier of H
xx "/\" f is Element of the carrier of (InclPoset (Ids H))
(SupMap H) . (xx "/\" f) is Element of the carrier of H
(SupMap H) . (X "/\" X1) is set
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema RelStr
Ids H is non empty set
the carrier of H is non empty set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of H : verum } is set
InclPoset (Ids H) is non empty strict V70() reflexive transitive antisymmetric non void with_suprema RelStr
SupMap H is non empty Relation-like the carrier of (InclPoset (Ids H)) -defined the carrier of H -valued Function-like V31( the carrier of (InclPoset (Ids H))) V33( the carrier of (InclPoset (Ids H)), the carrier of H) monotone Element of bool [: the carrier of (InclPoset (Ids H)), the carrier of H:]
the carrier of (InclPoset (Ids H)) is non empty set
[: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of (InclPoset (Ids H))
X is Element of the carrier of (InclPoset (Ids H))
{a,X} is non empty finite Element of bool the carrier of (InclPoset (Ids H))
bool the carrier of (InclPoset (Ids H)) is non empty cup-closed diff-closed preBoolean set
(SupMap H) .: {a,X} is non empty finite Element of bool the carrier of H
"\/" (((SupMap H) .: {a,X}),H) is Element of the carrier of H
"\/" ({a,X},(InclPoset (Ids H))) is Element of the carrier of (InclPoset (Ids H))
(SupMap H) . ("\/" ({a,X},(InclPoset (Ids H)))) is Element of the carrier of H
xx is non empty directed lower Element of bool the carrier of H
f is non empty directed lower Element of bool the carrier of H
xx "\/" f is non empty directed Element of bool the carrier of H
dom (SupMap H) is non empty Element of bool the carrier of (InclPoset (Ids H))
(SupMap H) . a is Element of the carrier of H
(SupMap H) . X is Element of the carrier of H
{((SupMap H) . a),((SupMap H) . X)} is non empty finite Element of bool the carrier of H
"\/" ({((SupMap H) . a),((SupMap H) . X)},H) is Element of the carrier of H
((SupMap H) . a) "\/" ((SupMap H) . X) is Element of the carrier of H
"\/" (f,H) is Element of the carrier of H
((SupMap H) . a) "\/" ("\/" (f,H)) is Element of the carrier of H
"\/" (xx,H) is Element of the carrier of H
("\/" (xx,H)) "\/" ("\/" (f,H)) is Element of the carrier of H
"\/" ((xx "\/" f),H) is Element of the carrier of H
downarrow (xx "\/" f) is non empty directed lower Element of bool the carrier of H
"\/" ((downarrow (xx "\/" f)),H) is Element of the carrier of H
(SupMap H) . (downarrow (xx "\/" f)) is set
a "\/" X is Element of the carrier of (InclPoset (Ids H))
(SupMap H) . (a "\/" X) is Element of the carrier of H
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
Ids H is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of H : verum } is set
InclPoset (Ids H) is non empty strict V70() reflexive transitive antisymmetric non void with_infima RelStr
SupMap H is non empty Relation-like the carrier of (InclPoset (Ids H)) -defined the carrier of H -valued Function-like V31( the carrier of (InclPoset (Ids H))) V33( the carrier of (InclPoset (Ids H)), the carrier of H) monotone Element of bool [: the carrier of (InclPoset (Ids H)), the carrier of H:]
the carrier of (InclPoset (Ids H)) is non empty set
[: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of (InclPoset (Ids H))
X is Element of the carrier of (InclPoset (Ids H))
{a,X} is non empty finite Element of bool the carrier of (InclPoset (Ids H))
bool the carrier of (InclPoset (Ids H)) is non empty cup-closed diff-closed preBoolean set
(SupMap H) .: {a,X} is non empty finite Element of bool the carrier of H
"/\" (((SupMap H) .: {a,X}),H) is Element of the carrier of H
"/\" ({a,X},(InclPoset (Ids H))) is Element of the carrier of (InclPoset (Ids H))
(SupMap H) . ("/\" ({a,X},(InclPoset (Ids H)))) is Element of the carrier of H
dom (SupMap H) is non empty Element of bool the carrier of (InclPoset (Ids H))
(SupMap H) . a is Element of the carrier of H
(SupMap H) . X is Element of the carrier of H
{((SupMap H) . a),((SupMap H) . X)} is non empty finite Element of bool the carrier of H
"/\" ({((SupMap H) . a),((SupMap H) . X)},H) is Element of the carrier of H
((SupMap H) . a) "/\" ((SupMap H) . X) is Element of the carrier of H
f is non empty directed lower Element of bool the carrier of H
"\/" (f,H) is Element of the carrier of H
((SupMap H) . a) "/\" ("\/" (f,H)) is Element of the carrier of H
xx is non empty directed lower Element of bool the carrier of H
"\/" (xx,H) is Element of the carrier of H
("\/" (xx,H)) "/\" ("\/" (f,H)) is Element of the carrier of H
xx "/\" f is non empty directed lower Element of bool the carrier of H
"\/" ((xx "/\" f),H) is Element of the carrier of H
(SupMap H) . (xx "/\" f) is set
a "/\" X is Element of the carrier of (InclPoset (Ids H))
(SupMap H) . (a "/\" X) is Element of the carrier of H
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
"\/" (a,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
downarrow a is non empty directed lower Element of bool the carrier of H
downarrow X is non empty directed lower Element of bool the carrier of H
(downarrow a) "/\" (downarrow X) is non empty directed lower Element of bool the carrier of H
"\/" ((downarrow a),H) is Element of the carrier of H
("\/" ((downarrow a),H)) "/\" ("\/" (X,H)) is Element of the carrier of H
"\/" ((downarrow X),H) is Element of the carrier of H
("\/" ((downarrow a),H)) "/\" ("\/" ((downarrow X),H)) is Element of the carrier of H
"\/" (((downarrow a) "/\" (downarrow X)),H) is Element of the carrier of H
downarrow ((downarrow a) "/\" (downarrow X)) is non empty directed lower Element of bool the carrier of H
"\/" ((downarrow ((downarrow a) "/\" (downarrow X))),H) is Element of the carrier of H
downarrow (a "/\" X) is non empty directed lower Element of bool the carrier of H
"\/" ((downarrow (a "/\" X)),H) is Element of the carrier of H
H is non empty V70() reflexive non void 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 directed NetStr over H
(H,X) is Element of 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
\\/ ( the mapping of X,H) is Element of the carrier of H
a "/\" (H,X) is Element of the carrier of H
netmap (X,H) 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:]
rng (netmap (X,H)) is non empty Element of bool the carrier of H
{a} "/\" (rng (netmap (X,H))) is non empty Element of bool the carrier of H
"\/" (({a} "/\" (rng (netmap (X,H)))),H) is Element of the carrier of H
"\/" ((rng (netmap (X,H))),H) is Element of the carrier of H
a "/\" ("\/" ((rng (netmap (X,H))),H)) 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
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 non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
a "/\" ("\/" (X,H)) is Element of the carrier of H
{a} "/\" X is non empty Element of bool the carrier of H
"\/" (({a} "/\" X),H) is Element of the carrier of H
[:X, the carrier of H:] is non empty Relation-like set
bool [:X, the carrier of H:] is non empty cup-closed diff-closed preBoolean set
id X is non empty Relation-like X -defined X -valued Function-like one-to-one V31(X) V33(X,X) Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] 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
the InternalRel of H |_2 X is Relation-like X -defined X -valued Element of bool [:X,X:]
the InternalRel of H /\ [:X,X:] is Relation-like the carrier of H -defined the carrier of H -valued set
X1 is non empty Relation-like X -defined the carrier of H -valued Function-like V31(X) V33(X, the carrier of H) Element of bool [:X, the carrier of H:]
NetStr(# X,( the InternalRel of H |_2 X),X1 #) is non empty strict NetStr over H
xx is non empty directed NetStr over H
netmap (xx,H) is non empty 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 is non empty set
[: the carrier of xx, the carrier of H:] is non empty Relation-like set
bool [: the carrier of xx, the carrier of H:] is non empty cup-closed diff-closed preBoolean set
the mapping of xx is non empty 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:]
\\/ ((netmap (xx,H)),H) is Element of the carrier of H
(H,xx) is Element of the carrier of H
\\/ ( the mapping of xx,H) is Element of the carrier of H
X1 .: X is Element of bool the carrier of H
rng (netmap (xx,H)) is non empty Element of bool the carrier of H
a "/\" (\\/ ((netmap (xx,H)),H)) is Element of the carrier of H
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
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean 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
"\/" (a,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
[:a,X:] is non empty Relation-like directed Element of bool the carrier of [:H,H:]
bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set
(H) . (("\/" (a,H)),("\/" (X,H))) is set
[("\/" (a,H)),("\/" (X,H))] is V1() set
{("\/" (a,H)),("\/" (X,H))} is non empty finite set
{("\/" (a,H))} is non empty trivial finite V53(1) set
{{("\/" (a,H)),("\/" (X,H))},{("\/" (a,H))}} is non empty finite V50() set
(H) . [("\/" (a,H)),("\/" (X,H))] is set
"\/" ([:a,X:],[:H,H:]) is Element of the carrier of [:H,H:]
(H) . ("\/" ([:a,X:],[:H,H:])) is Element of the carrier of H
(H) .: [:a,X:] is non empty Element of bool the carrier of H
"\/" (((H) .: [:a,X:]),H) is Element of the carrier of H
H is non empty V70() reflexive antisymmetric 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
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 non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
a "/\" ("\/" (X,H)) is Element of the carrier of H
{a} "/\" X is non empty 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
("\/" ({a},H)) "/\" ("\/" (X,H)) is Element of the carrier of H
H is non empty V70() reflexive antisymmetric 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 Element of the carrier of H
{a} is non empty trivial finite V53(1) Element of bool the carrier of H
X is non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
{a} "/\" X is non empty 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
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
[:H,H:] is non empty strict V70() reflexive transitive antisymmetric up-complete non void with_infima RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
bool the carrier of [:H,H:] is non empty cup-closed diff-closed preBoolean set
a is Element of bool the carrier of [:H,H:]
X is non empty directed Element of bool the carrier of [:H,H:]
proj1 X is Element of bool the carrier of H
proj2 X is Element of bool the carrier of H
(H) .: a is Element of bool the carrier of H
"\/" (((H) .: a),H) is Element of the carrier of H
"\/" (a,[:H,H:]) is Element of the carrier of [:H,H:]
(H) . ("\/" (a,[:H,H:])) is Element of the carrier of H
xx is non empty directed Element of bool the carrier of H
"\/" (xx,H) is Element of the carrier of H
X1 is non empty directed Element of bool the carrier of H
(H) .: X is non empty Element of bool the carrier of H
{("\/" (xx,H))} is non empty trivial finite V53(1) Element of bool the carrier of H
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in X1 & b₂ in {("\/" (xx,H))} ) } is set
f is non empty set
y is set
Y is Element of the carrier of H
z is Element of the carrier of H
Y "/\" z is Element of the carrier of H
{ ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
"\/" ( { ("\/" (b₁,H)) where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } ,H) is Element of the carrier of H
{ b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } is set
"\/" ((union { b₁ where b₁ is non empty directed Element of bool the carrier of H : S₁[b₁] } ),H) is Element of the carrier of H
y is Element of bool the carrier of H
{ ("\/" (({b₁} "/\" xx),H)) where b₁ is Element of the carrier of H : b₁ in X1 } is set
Y is set
z is Element of the carrier of H
y is Element of the carrier of H
z "/\" y is Element of the carrier of H
z "/\" ("\/" (xx,H)) is Element of the carrier of H
{z} is non empty trivial finite V53(1) Element of bool the carrier of H
{z} "/\" xx is non empty Element of bool the carrier of H
"\/" (({z} "/\" xx),H) is Element of the carrier of H
Y is set
z is Element of the carrier of H
{z} is non empty trivial finite V53(1) Element of bool the carrier of H
{z} "/\" xx is non empty Element of bool the carrier of H
"\/" (({z} "/\" xx),H) is Element of the carrier of H
z "/\" ("\/" (xx,H)) is Element of the carrier of H
X1 "/\" xx is non empty directed Element of bool the carrier of H
"\/" ((X1 "/\" xx),H) is Element of the carrier of H
"\/" ( { ("\/" (({b₁} "/\" xx),H)) where b₁ is Element of the carrier of H : b₁ in X1 } ,H) is Element of the carrier of H
{("\/" (xx,H))} "/\" X1 is non empty Element of bool the carrier of H
"\/" (({("\/" (xx,H))} "/\" X1),H) is Element of the carrier of H
"\/" (X1,H) is Element of the carrier of H
("\/" (X1,H)) "/\" ("\/" (xx,H)) is Element of the carrier of H
(H) . (("\/" (X1,H)),("\/" (xx,H))) is set
[("\/" (X1,H)),("\/" (xx,H))] is V1() set
{("\/" (X1,H)),("\/" (xx,H))} is non empty finite set
{("\/" (X1,H))} is non empty trivial finite V53(1) set
{{("\/" (X1,H)),("\/" (xx,H))},{("\/" (X1,H))}} is non empty finite V50() set
(H) . [("\/" (X1,H)),("\/" (xx,H))] 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 is Element of the carrier of H
X is set
[:X, the carrier of H:] is Relation-like set
bool [:X, the carrier of H:] is non empty cup-closed diff-closed preBoolean set
X1 is Relation-like X -defined the carrier of H -valued Function-like V31(X) V33(X, the carrier of H) Element of bool [:X, the carrier of H:]
\\/ (X1,H) is Element of the carrier of H
a "/\" (\\/ (X1,H)) is Element of the carrier of H
(H,X,X1) is non empty directed monotone eventually-directed NetStr over H
(H,a,(H,X,X1)) is non empty strict directed NetStr over H
(H,(H,a,(H,X,X1))) is Element of the carrier of H
the mapping of (H,a,(H,X,X1)) is non empty Relation-like the carrier of (H,a,(H,X,X1)) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,(H,X,X1))) V33( the carrier of (H,a,(H,X,X1)), the carrier of H) Element of bool [: the carrier of (H,a,(H,X,X1)), the carrier of H:]
the carrier of (H,a,(H,X,X1)) is non empty set
[: the carrier of (H,a,(H,X,X1)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (H,a,(H,X,X1)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of (H,a,(H,X,X1)),H) is Element of the carrier of H
Fin X is non empty cup-closed diff-closed preBoolean set
f is finite Element of Fin X
X1 .: f is finite Element of bool the carrier of H
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
rng X1 is Element of bool the carrier of H
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
netmap ((H,X,X1),H) is non empty Relation-like the carrier of (H,X,X1) -defined the carrier of H -valued Function-like V31( the carrier of (H,X,X1)) V33( the carrier of (H,X,X1), the carrier of H) Element of bool [: the carrier of (H,X,X1), the carrier of H:]
the carrier of (H,X,X1) is non empty set
[: the carrier of (H,X,X1), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (H,X,X1), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
the mapping of (H,X,X1) is non empty Relation-like the carrier of (H,X,X1) -defined the carrier of H -valued Function-like V31( the carrier of (H,X,X1)) V33( the carrier of (H,X,X1), the carrier of H) Element of bool [: the carrier of (H,X,X1), the carrier of H:]
rng (netmap ((H,X,X1),H)) is non empty Element of bool the carrier of H
(H,(H,X,X1)) is Element of the carrier of H
\\/ ( the mapping of (H,X,X1),H) is Element of the carrier of H
a "/\" (H,(H,X,X1)) is Element of the carrier of H
{a} is non empty trivial finite V53(1) Element of bool the carrier of H
{a} "/\" (rng (netmap ((H,X,X1),H))) is non empty Element of bool the carrier of H
"\/" (({a} "/\" (rng (netmap ((H,X,X1),H)))),H) is Element of the carrier of H
rng the mapping of (H,a,(H,X,X1)) is non empty Element of bool the carrier of H
"\/" ((rng the mapping of (H,a,(H,X,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 non void with_suprema with_infima complete 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 directed NetStr over H
(H,X) is Element of 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
\\/ ( the mapping of X,H) is Element of the carrier of H
a "/\" (H,X) is Element of the carrier of H
netmap (X,H) 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:]
rng (netmap (X,H)) is non empty Element of bool the carrier of H
{a} "/\" (rng (netmap (X,H))) is non empty Element of bool the carrier of H
"\/" (({a} "/\" (rng (netmap (X,H)))),H) is Element of the carrier of H
(H, the carrier of X, the mapping of X) is non empty directed monotone eventually-directed NetStr over H
the mapping of (H, the carrier of X, the mapping of X) is non empty Relation-like the carrier of (H, the carrier of X, the mapping of X) -defined the carrier of H -valued Function-like V31( the carrier of (H, the carrier of X, the mapping of X)) V33( the carrier of (H, the carrier of X, the mapping of X), the carrier of H) Element of bool [: the carrier of (H, the carrier of X, the mapping of X), the carrier of H:]
the carrier of (H, the carrier of X, the mapping of X) is non empty set
[: the carrier of (H, the carrier of X, the mapping of X), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (H, the carrier of X, the mapping of X), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
xx is non empty directed Element of bool the carrier of H
X1 is non empty directed Element of bool the carrier of H
xx "/\" X1 is non empty directed Element of bool the carrier of H
(H,a,(H, the carrier of X, the mapping of X)) is non empty strict directed NetStr over H
the mapping of (H,a,(H, the carrier of X, the mapping of X)) is non empty Relation-like the carrier of (H,a,(H, the carrier of X, the mapping of X)) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,(H, the carrier of X, the mapping of X))) V33( the carrier of (H,a,(H, the carrier of X, the mapping of X)), the carrier of H) Element of bool [: the carrier of (H,a,(H, the carrier of X, the mapping of X)), the carrier of H:]
the carrier of (H,a,(H, the carrier of X, the mapping of X)) is non empty set
[: the carrier of (H,a,(H, the carrier of X, the mapping of X)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (H,a,(H, the carrier of X, the mapping of X)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
rng the mapping of (H,a,(H, the carrier of X, the mapping of X)) is non empty Element of bool the carrier of H
a is Element of the carrier of H
rng the mapping of (H, the carrier of X, the mapping of X) is non empty Element of bool the carrier of H
{a} "/\" (rng the mapping of (H, the carrier of X, the mapping of X)) is non empty Element of bool the carrier of H
{ (a "/\" b₁) where b₁ is Element of the carrier of H : b₁ in rng the mapping of (H, the carrier of X, the mapping of X) } is set
y is Element of the carrier of H
a "/\" y is Element of the carrier of H
Y is set
the mapping of X .: Y is Element of bool the carrier of H
netmap ((H, the carrier of X, the mapping of X),H) is non empty Relation-like the carrier of (H, the carrier of X, the mapping of X) -defined the carrier of H -valued Function-like V31( the carrier of (H, the carrier of X, the mapping of X)) V33( the carrier of (H, the carrier of X, the mapping of X), the carrier of H) Element of bool [: the carrier of (H, the carrier of X, the mapping of X), the carrier of H:]
rng (netmap ((H, the carrier of X, the mapping of X),H)) is non empty Element of bool the carrier of H
rng the mapping of X is non empty Element of bool the carrier of H
finsups (rng the mapping of X) is non empty directed Element of bool the carrier of H
bool (rng the mapping of X) is non empty cup-closed diff-closed preBoolean set
{ ("\/" (b₁,H)) where b₁ is finite Element of bool (rng the mapping of X) : ex_sup_of b₁,H } is set
Y is finite Element of bool (rng the mapping of X)
"\/" (Y,H) is Element of the carrier of H
z is Element of the carrier of H
a "/\" z is Element of the carrier of H
xx "/\" (rng the mapping of X) is non empty Element of bool the carrier of H
"\/" ((xx "/\" (rng the mapping of X)),H) is Element of the carrier of H
netmap ((H,a,(H, the carrier of X, the mapping of X)),H) is non empty Relation-like the carrier of (H,a,(H, the carrier of X, the mapping of X)) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,(H, the carrier of X, the mapping of X))) V33( the carrier of (H,a,(H, the carrier of X, the mapping of X)), the carrier of H) Element of bool [: the carrier of (H,a,(H, the carrier of X, the mapping of X)), the carrier of H:]
rng (netmap ((H,a,(H, the carrier of X, the mapping of X)),H)) is non empty Element of bool the carrier of H
(H,(H,a,(H, the carrier of X, the mapping of X))) is Element of the carrier of H
\\/ ( the mapping of (H,a,(H, the carrier of X, the mapping of X)),H) is Element of the carrier of H
"\/" ((rng the mapping of (H,a,(H, the carrier of X, the mapping of X))),H) is Element of the carrier of H
\\/ ((netmap (X,H)),H) is Element of the carrier of H
a "/\" (\\/ ((netmap (X,H)),H)) is Element of the carrier of H
"\/" ((rng (netmap (X,H))),H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima RelStr
Ids H is non empty set
the carrier of H is non empty set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of H : verum } is set
InclPoset (Ids H) is non empty strict V70() reflexive transitive antisymmetric non void with_suprema with_infima RelStr
SupMap H is non empty Relation-like the carrier of (InclPoset (Ids H)) -defined the carrier of H -valued Function-like V31( the carrier of (InclPoset (Ids H))) V33( the carrier of (InclPoset (Ids H)), the carrier of H) monotone join-preserving Element of bool [: the carrier of (InclPoset (Ids H)), the carrier of H:]
the carrier of (InclPoset (Ids H)) is non empty set
[: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids 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,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
X1 is Element of the carrier of H
xx is non empty directed Element of bool the carrier of H
"\/" (xx,H) is Element of the carrier of H
{X1} is non empty trivial finite V53(1) Element of bool the carrier of H
{X1} "/\" xx is non empty Element of bool the carrier of H
"\/" (({X1} "/\" xx),H) is Element of the carrier of H
[:H,H:] is non empty strict V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is non empty directed lower Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed lower Element of bool 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 is non empty directed lower Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
a is non empty directed lower Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed lower Element of bool 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 is non empty directed lower Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
a is non empty directed Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima () () RelStr
Ids H is non empty set
the carrier of H is non empty set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of H : verum } is set
InclPoset (Ids H) is non empty strict V70() reflexive transitive antisymmetric non void with_suprema with_infima RelStr
SupMap H is non empty Relation-like the carrier of (InclPoset (Ids H)) -defined the carrier of H -valued Function-like V31( the carrier of (InclPoset (Ids H))) V33( the carrier of (InclPoset (Ids H)), the carrier of H) monotone join-preserving Element of bool [: the carrier of (InclPoset (Ids H)), the carrier of H:]
the carrier of (InclPoset (Ids H)) is non empty set
[: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema 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
Ids H is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of H : verum } is set
InclPoset (Ids H) is non empty strict V70() reflexive transitive antisymmetric non void with_suprema with_infima RelStr
SupMap H is non empty Relation-like the carrier of (InclPoset (Ids H)) -defined the carrier of H -valued Function-like V31( the carrier of (InclPoset (Ids H))) V33( the carrier of (InclPoset (Ids H)), the carrier of H) monotone join-preserving Element of bool [: the carrier of (InclPoset (Ids H)), the carrier of H:]
the carrier of (InclPoset (Ids H)) is non empty set
[: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids H)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is non empty directed lower Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed lower Element of bool 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 is non empty directed lower Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
a is non empty directed Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema 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 lower Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed lower Element of bool 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 is non empty directed lower Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
a is non empty directed Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of H
"\/" ((a "/\" X),H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema 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 Element of the carrier of H
X is non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
{a} is non empty trivial finite V53(1) Element of bool the carrier of H
{a} "/\" X is non empty Element of bool the carrier of H
"\/" (({a} "/\" X),H) is Element of the carrier of H
a is Element of the carrier of H
X is non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
{a} is non empty trivial finite V53(1) Element of bool the carrier of H
{a} "/\" X is non empty Element of bool the carrier of H
"\/" (({a} "/\" X),H) is Element of the carrier of H
[:H,H:] is non empty strict V70() reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,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,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of 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 up-complete non void with_infima RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], the carrier of H:] is non empty cup-closed diff-closed preBoolean set
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of H
X is non empty directed Element of bool the carrier of H
"\/" (X,H) is Element of the carrier of H
{a} is non empty trivial finite V53(1) Element of bool the carrier of H
{a} "/\" X is non empty Element of bool the carrier of H
"\/" (({a} "/\" X),H) is Element of the carrier of H
a is non empty directed Element of bool the carrier of H
"\/" (a,H) is Element of the carrier of H
X is non empty directed Element of bool 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 is non empty directed Element of bool the carrier of 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 up-complete non void with_infima RelStr
(H) is non empty Relation-like the carrier of [:H,H:] -defined the carrier of H -valued Function-like V31( the carrier of [:H,H:]) V33( the carrier of [:H,H:], the carrier of H) monotone Element of bool [: the carrier of [:H,H:], the carrier of H:]
the carrier of [:H,H:] is non empty set
the carrier of H is non empty set
[: the carrier of [:H,H:], the carrier of H:] is non empty Relation-like set
bool [: the carrier of [:H,H:], 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
X is non empty directed NetStr over H
a is Element of the carrier of H
(H,X) is Element of 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
\\/ ( the mapping of X,H) is Element of the carrier of H
a "/\" (H,X) 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
netmap (X,H) 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:]
rng (netmap (X,H)) is non empty Element of bool the carrier of H
{a} "/\" (rng (netmap (X,H))) is non empty Element of bool the carrier of H
"\/" (({a} "/\" (rng (netmap (X,H)))),H) is Element of the carrier of H
H is non empty V70() reflexive transitive 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
X is non empty directed NetStr over H
a is Element of the carrier of H
(H,X) is Element of 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
\\/ ( the mapping of X,H) is Element of the carrier of H
a "/\" (H,X) 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
netmap (X,H) 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:]
rng (netmap (X,H)) is non empty Element of bool the carrier of H
{a} "/\" (rng (netmap (X,H))) is non empty Element of bool the carrier of H
"\/" (({a} "/\" (rng (netmap (X,H)))),H) is Element of the carrier of H
X is set
[:X, the carrier of H:] is Relation-like set
bool [:X, the carrier of H:] is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of H
X1 is Relation-like X -defined the carrier of H -valued Function-like V31(X) V33(X, the carrier of H) Element of bool [:X, the carrier of H:]
\\/ (X1,H) is Element of the carrier of H
a "/\" (\\/ (X1,H)) is Element of the carrier of H
(H,X,X1) is non empty directed monotone eventually-directed NetStr over H
(H,a,(H,X,X1)) is non empty strict directed NetStr over H
(H,(H,a,(H,X,X1))) is Element of the carrier of H
the mapping of (H,a,(H,X,X1)) is non empty Relation-like the carrier of (H,a,(H,X,X1)) -defined the carrier of H -valued Function-like V31( the carrier of (H,a,(H,X,X1))) V33( the carrier of (H,a,(H,X,X1)), the carrier of H) Element of bool [: the carrier of (H,a,(H,X,X1)), the carrier of H:]
the carrier of (H,a,(H,X,X1)) is non empty set
[: the carrier of (H,a,(H,X,X1)), the carrier of H:] is non empty Relation-like set
bool [: the carrier of (H,a,(H,X,X1)), the carrier of H:] is non empty cup-closed diff-closed preBoolean set
\\/ ( the mapping of (H,a,(H,X,X1)),H) is Element of the carrier of H
X is non empty directed NetStr over H
a is Element of the carrier of H
(H,X) is Element of 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
\\/ ( the mapping of X,H) is Element of the carrier of H
a "/\" (H,X) 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
netmap (X,H) 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:]
rng (netmap (X,H)) is non empty Element of bool the carrier of H
{a} "/\" (rng (netmap (X,H))) is non empty Element of bool the carrier of H
"\/" (({a} "/\" (rng (netmap (X,H)))),H) is Element of the carrier of H
H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima () () RelStr
the carrier of H is non empty 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
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
X is 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 non empty Element of bool the carrier of H
(a "/\") .: X1 is non empty Element of bool the carrier of H
xx is Element of the carrier of H
f is non empty directed Element of bool the carrier of H
"\/" (f,H) is Element of the carrier of H
{xx} is non empty trivial finite V53(1) Element of bool the carrier of H
{xx} "/\" f is non empty Element of bool the carrier of H
"\/" (({xx} "/\" f),H) is Element of the carrier of H
{ (a "/\" b₁) where b₁ is Element of the carrier of H : b₁ in X } is set
"\/" ( { (a "/\" b₁) where b₁ is Element of the carrier of H : b₁ in X } ,H) is Element of the carrier of H
{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
H is non empty V70() reflexive transitive antisymmetric up-complete non void with_infima () () RelStr
the carrier of H is non empty 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
H is non empty V70() reflexive transitive 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 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
bool the carrier of H is non empty cup-closed diff-closed preBoolean set
X 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
X "/\" ("\/" (a,H)) is Element of the carrier of H
{ (X "/\" b₁) where b₁ is Element of the carrier of H : b₁ in a } is set
"\/" ( { (X "/\" b₁) where b₁ is Element of the carrier of H : b₁ in a } ,H) is Element of the carrier of H
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
X1 is non empty directed Element of bool the carrier of H
H is non empty V70() reflexive transitive antisymmetric non void RelStr
H is non empty V70() reflexive transitive antisymmetric non void RelStr