REAL is set
NAT is non empty non trivial V23() V24() V25() non finite V42() V43() countable denumerable Element of K10(REAL)
K10(REAL) is non empty set
NAT is non empty non trivial V23() V24() V25() non finite V42() V43() countable denumerable set
K10(NAT) is non empty non trivial non finite set
K10(NAT) is non empty non trivial non finite set
1 is non empty ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
K11(1,1) is non empty finite countable set
K10(K11(1,1)) is non empty finite V41() countable set
K11(K11(1,1),1) is non empty finite countable set
K10(K11(K11(1,1),1)) is non empty finite V41() countable set
K11(K11(1,1),REAL) is set
K10(K11(K11(1,1),REAL)) is non empty set
K11(REAL,REAL) is set
K11(K11(REAL,REAL),REAL) is set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
2 is non empty ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
K11(2,2) is non empty finite countable set
K11(K11(2,2),REAL) is set
K10(K11(K11(2,2),REAL)) is non empty set
COMPLEX is set
RAT is set
INT is set
K10(K11(REAL,REAL)) is non empty set
K392() is non empty V122() L10()
the carrier of K392() is non empty set
<REAL,+> is non empty V122() V144() V145() V146() V148() left-invertible right-invertible V197() left-cancelable right-cancelable V200() L10()
K398() is non empty V122() V146() V148() left-cancelable right-cancelable V200() SubStr of <REAL,+>
<NAT,+> is non empty V122() V144() V146() V148() left-cancelable right-cancelable V200() uniquely-decomposable SubStr of K398()
<REAL,*> is non empty V122() V144() V146() V148() L10()
<NAT,*> is non empty V122() V144() V146() V148() uniquely-decomposable SubStr of <REAL,*>
K443() is set
{} is empty Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) V87() countable set
the empty Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) V87() countable set is empty Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) V87() countable set
{{}} is non empty trivial finite V41() V44(1) countable set
K363({{}}) is M14({{}})
K11(K363({{}}),{{}}) is set
K10(K11(K363({{}}),{{}})) is non empty set
K127(K363({{}}),{{}}) is set
union {} is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable set
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
T is non empty V233() reflexive antisymmetric RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
K10( the carrier of T) is non empty set
{x} is non empty trivial finite V44(1) countable Element of K10( the carrier of T)
"\/" ({x},T) is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive transitive RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
X is Element of the carrier of T
a is Element of the carrier of T
K10( the carrier of T) is non empty set
Y is non empty directed Element of K10( the carrier of T)
"\/" (Y,T) is Element of the carrier of T
y is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric RelStr
the carrier of T is non empty set
L is Element of the carrier of T
X is Element of the carrier of T
x is Element of the carrier of T
{L,x} is non empty finite countable Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
L "\/" x is Element of the carrier of T
{ b1 where b1 is Element of the carrier of T : ( L <= b1 & x <= b1 ) } is set
Y is set
y is Element of the carrier of T
Y is Element of K10( the carrier of T)
y is Element of the carrier of T
y is Element of the carrier of T
W is Element of the carrier of T
Z is Element of the carrier of T
y is Element of the carrier of T
a is non empty directed Element of K10( the carrier of T)
"\/" (a,T) is Element of the carrier of T
Y is Element of the carrier of T
y is Element of the carrier of T
y is Element of the carrier of T
T is non empty V233() reflexive antisymmetric lower-bounded RelStr
the carrier of T is non empty set
Bottom T is Element of the carrier of T
"\/" ({},T) is Element of the carrier of T
L is Element of the carrier of T
K10( the carrier of T) is non empty set
x is non empty directed Element of K10( the carrier of T)
"\/" (x,T) is Element of the carrier of T
the Element of x is Element of x
a is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive antisymmetric RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
L is Element of the carrier of T
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
x is set
X is Element of the carrier of T
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,L,b1) } is set
x is set
X is Element of the carrier of T
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
(T,x) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,x) } is set
X is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
(T,x) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,x,b1) } is set
X is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive antisymmetric RelStr
the carrier of T is non empty set
x is Element of the carrier of T
L is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
T is non empty V233() reflexive antisymmetric RelStr
the carrier of T is non empty set
x is Element of the carrier of T
L is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,L,b1) } is set
T is non empty V233() reflexive antisymmetric RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
downarrow L is non empty directed Element of K10( the carrier of T)
{L} is non empty trivial finite V44(1) countable Element of K10( the carrier of T)
downarrow {L} is non empty Element of K10( the carrier of T)
(T,L) is Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,L,b1) } is set
uparrow L is non empty filtered Element of K10( the carrier of T)
uparrow {L} is non empty Element of K10( the carrier of T)
x is set
X is Element of the carrier of T
x is set
X is Element of the carrier of T
T is non empty V233() reflexive transitive RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
(T,x) is Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,b1,x) } is set
(T,x) is Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,x,b1) } is set
(T,L) is Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,L,b1) } is set
X is set
a is Element of the carrier of T
X is set
a is Element of the carrier of T
T is non empty V233() reflexive antisymmetric lower-bounded RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
Bottom T is Element of the carrier of T
"\/" ({},T) is Element of the carrier of T
T is non empty V233() reflexive transitive RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
x is Element of the carrier of T
X is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,L,b1) } is set
x is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric with_suprema RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
x is Element of the carrier of T
X is Element of the carrier of T
{x,X} is non empty finite countable Element of K10( the carrier of T)
x "\/" X is Element of the carrier of T
a is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric lower-bounded with_infima /\-complete RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is non empty lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
x is Element of the carrier of T
X is Element of the carrier of T
{x,X} is non empty finite countable Element of K10( the carrier of T)
x "\/" X is Element of the carrier of T
a is Element of the carrier of T
T is non empty connected RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is Element of K10( the carrier of T)
x is Element of the carrier of T
X is Element of the carrier of T
x is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric connected RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is directed filtered Element of K10( the carrier of T)
the set is set
{ the set } is non empty trivial finite V44(1) countable set
K11({ the set },{ the set }) is non empty finite countable set
K10(K11({ the set },{ the set })) is non empty finite V41() countable set
the V31({ the set }) finite countable V221() V224() V228() Element of K10(K11({ the set },{ the set })) is V31({ the set }) finite countable V221() V224() V228() Element of K10(K11({ the set },{ the set }))
RelStr(# { the set }, the V31({ the set }) finite countable V221() V224() V228() Element of K10(K11({ the set },{ the set })) #) is non empty trivial finite 1 -element strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete connected up-complete /\-complete RelStr
T is non empty V233() reflexive transitive antisymmetric connected up-complete RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
K10( the carrier of T) is non empty set
X is non empty directed filtered Element of K10( the carrier of T)
"\/" (X,T) is Element of the carrier of T
a is Element of the carrier of T
T is non empty V233() reflexive antisymmetric RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
T is non empty V233() reflexive antisymmetric lower-bounded RelStr
Bottom T is Element of the carrier of T
the carrier of T is non empty set
"\/" ({},T) is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric up-complete RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is non empty finite countable directed Element of K10( the carrier of T)
"\/" (L,T) is Element of the carrier of T
x is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric up-complete RelStr
the carrier of T is non empty set
L is Element of the carrier of T
K10( the carrier of T) is non empty set
x is non empty directed Element of K10( the carrier of T)
"\/" (x,T) is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
X is Element of K10( the carrier of T)
"\/" (X,T) is Element of the carrier of T
K10(X) is non empty set
a is Element of K10( the carrier of T)
Y is finite countable Element of K10(X)
"\/" (Y,T) is Element of the carrier of T
Y is finite countable Element of K10(X)
"\/" ({},T) is Element of the carrier of T
Y is non empty directed Element of K10( the carrier of T)
"\/" (Y,T) is Element of the carrier of T
y is Element of the carrier of T
y is finite countable Element of K10(X)
"\/" (y,T) is Element of the carrier of T
W is finite countable Element of K10( the carrier of T)
"\/" (W,T) is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
x is Element of the carrier of T
L is Element of the carrier of T
X is non empty directed Element of K10( the carrier of T)
"\/" (X,T) is Element of the carrier of T
a is finite countable Element of K10( the carrier of T)
"\/" (a,T) is Element of the carrier of T
K10(X) is non empty set
Y is finite countable Element of K10(X)
y is Element of the carrier of T
T is non empty V233() reflexive transitive RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
X is non empty directed lower Element of K10( the carrier of T)
"\/" (X,T) is Element of the carrier of T
a is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric up-complete RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
x is Element of the carrier of T
L is Element of the carrier of T
X is non empty directed Element of K10( the carrier of T)
"\/" (X,T) is Element of the carrier of T
downarrow X is non empty directed lower Element of K10( the carrier of T)
"\/" ((downarrow X),T) is Element of the carrier of T
a is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
X is non empty directed lower Element of K10( the carrier of T)
"\/" (X,T) is Element of the carrier of T
a is Element of the carrier of T
{x} is non empty trivial finite V44(1) countable Element of K10( the carrier of T)
X is non empty directed lower Element of K10( the carrier of T)
{x} "/\" X is Element of K10( the carrier of T)
finsups ({x} "/\" X) is non empty directed Element of K10( the carrier of T)
K10(({x} "/\" X)) is non empty set
{ ("\/" (b1,T)) where b1 is finite countable Element of K10(({x} "/\" X)) : ex_sup_of b1,T } is set
"\/" (X,T) is Element of the carrier of T
x "/\" ("\/" (X,T)) is Element of the carrier of T
"\/" (({x} "/\" X),T) is Element of the carrier of T
"\/" ((finsups ({x} "/\" X)),T) is Element of the carrier of T
downarrow (finsups ({x} "/\" X)) is non empty directed lower Element of K10( the carrier of T)
"\/" ((downarrow (finsups ({x} "/\" X))),T) is Element of the carrier of T
a is Element of the carrier of T
Y is finite countable Element of K10(({x} "/\" X))
"\/" (Y,T) is Element of the carrier of T
the Element of X is Element of X
y is Element of the carrier of T
{y} is non empty trivial finite V44(1) countable Element of K10( the carrier of T)
"\/" ({y},T) is Element of the carrier of T
"\/" ({},T) is Element of the carrier of T
W is set
{ (x "/\" b1) where b1 is Element of the carrier of T : b1 in X } is set
Z is Element of the carrier of T
x "/\" Z is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is non empty Element of K10( the carrier of T)
the InternalRel of T is V31( the carrier of T) V221() V224() V228() Element of K10(K11( the carrier of T, the carrier of T))
K11( the carrier of T, the carrier of T) is non empty set
K10(K11( the carrier of T, the carrier of T)) is non empty set
x is set
X is Element of the carrier of T
a is Element of the carrier of T
Y is set
y is set
[x,y] is set
{x,y} is non empty finite countable set
{x} is non empty trivial finite V44(1) countable set
{{x,y},{x}} is non empty finite V41() countable set
x is Relation-like Function-like set
dom x is set
rng x is set
the Element of L is Element of L
{ ((iter (x,b1)) . the Element of L) where b1 is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT : verum } is set
x . the Element of L is set
y is Element of the carrier of T
x . y is set
[y,(x . y)] is set
{y,(x . y)} is non empty finite countable set
{y} is non empty trivial finite V44(1) countable set
{{y,(x . y)},{y}} is non empty finite V41() countable set
y is Element of the carrier of T
iter (x,1) is Relation-like Function-like set
(iter (x,1)) . y is set
W is set
Z is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,Z) is Relation-like Function-like set
(iter (x,Z)) . y is set
dom (iter (x,Z)) is set
rng (iter (x,Z)) is set
Z is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,Z) is Relation-like Function-like set
(iter (x,Z)) . y is set
W is Element of K10( the carrier of T)
0 is empty Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) V87() countable Element of NAT
Z + 0 is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,(Z + 0)) is Relation-like Function-like set
(iter (x,(Z + 0))) . y is set
F is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
Z + F is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,(Z + F)) is Relation-like Function-like set
(iter (x,(Z + F))) . y is set
F + 1 is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
Z + (F + 1) is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,(Z + (F + 1))) is Relation-like Function-like set
(iter (x,(Z + (F + 1)))) . y is set
ZZ is Element of the carrier of T
ZZ is Element of the carrier of T
rng (iter (x,(Z + F))) is set
dom (iter (x,(Z + F))) is set
x . ZZ is set
FZ is Element of the carrier of T
F + Z is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
(F + Z) + 1 is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,((F + Z) + 1)) is Relation-like Function-like set
iter (x,(F + Z)) is Relation-like Function-like set
(iter (x,(F + Z))) * x is Relation-like Function-like set
[ZZ,FZ] is Element of K11( the carrier of T, the carrier of T)
{ZZ,FZ} is non empty finite countable set
{ZZ} is non empty trivial finite V44(1) countable set
{{ZZ,FZ},{ZZ}} is non empty finite V41() countable set
F is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
ZZ is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable set
Z + ZZ is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
ZZ is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
Z + ZZ is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,(Z + ZZ)) is Relation-like Function-like set
(iter (x,(Z + ZZ))) . y is set
FZ is Element of the carrier of T
FF is Element of the carrier of T
iter (x,F) is Relation-like Function-like set
(iter (x,F)) . y is set
A is Element of the carrier of T
G is Element of the carrier of T
Z is Element of the carrier of T
ZZ is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,ZZ) is Relation-like Function-like set
(iter (x,ZZ)) . y is set
F is Element of the carrier of T
ZZ is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,ZZ) is Relation-like Function-like set
(iter (x,ZZ)) . y is set
"\/" (W,T) is Element of the carrier of T
Z is finite countable Element of K10( the carrier of T)
"\/" (Z,T) is Element of the carrier of T
"\/" ({},T) is Element of the carrier of T
F is set
ZZ is set
"\/" (ZZ,T) is Element of the carrier of T
{F} is non empty trivial finite V44(1) countable set
ZZ \/ {F} is non empty set
"\/" ((ZZ \/ {F}),T) is Element of the carrier of T
"\/" ({F},T) is Element of the carrier of T
("\/" (ZZ,T)) "\/" ("\/" ({F},T)) is Element of the carrier of T
ZZ is Element of the carrier of T
{ZZ} is non empty trivial finite V44(1) countable Element of K10( the carrier of T)
"\/" ({ZZ},T) is Element of the carrier of T
("\/" (ZZ,T)) "\/" ZZ is Element of the carrier of T
ZZ "\/" ("\/" (ZZ,T)) is Element of the carrier of T
F is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,F) is Relation-like Function-like set
(iter (x,F)) . y is set
x . ("\/" (Z,T)) is set
[("\/" (Z,T)),(x . ("\/" (Z,T)))] is set
{("\/" (Z,T)),(x . ("\/" (Z,T)))} is non empty finite countable set
{("\/" (Z,T))} is non empty trivial finite V44(1) countable set
{{("\/" (Z,T)),(x . ("\/" (Z,T)))},{("\/" (Z,T))}} is non empty finite V41() countable set
F + 1 is ext-real V23() V24() V25() V29() V30() finite V42() V87() countable Element of NAT
iter (x,(F + 1)) is Relation-like Function-like set
(iter (x,F)) * x is Relation-like Function-like set
dom (iter (x,F)) is set
ZZ is Element of the carrier of T
(iter (x,(F + 1))) . y is set
L is Element of the carrier of T
x is non empty directed Element of K10( the carrier of T)
"\/" (x,T) is Element of the carrier of T
X is Element of the carrier of T
a is Element of the carrier of T
Y is Element of the carrier of T
T is non empty trivial finite 1 -element V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete connected up-complete /\-complete RelStr
the carrier of T is non empty trivial finite V44(1) countable set
L is Element of the carrier of T
(T,L) is non empty trivial finite V44(1) countable directed filtered lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty finite V41() countable set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
"\/" ((T,L),T) is Element of the carrier of T
T is non empty V233() reflexive RelStr
T is non empty V233() reflexive transitive antisymmetric lower-bounded with_suprema RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is non empty directed lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
x is Element of the carrier of T
(T,x) is non empty directed lower Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,b1,x) } is set
the set is set
{ the set } is non empty trivial finite V44(1) countable set
K11({ the set },{ the set }) is non empty finite countable set
K10(K11({ the set },{ the set })) is non empty finite V41() countable set
the V31({ the set }) finite countable V221() V224() V228() Element of K10(K11({ the set },{ the set })) is V31({ the set }) finite countable V221() V224() V228() Element of K10(K11({ the set },{ the set }))
RelStr(# { the set }, the V31({ the set }) finite countable V221() V224() V228() Element of K10(K11({ the set },{ the set })) #) is non empty trivial finite 1 -element strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete connected up-complete /\-complete () () RelStr
T is non empty V233() reflexive up-complete () () RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
T is non empty V233() reflexive transitive antisymmetric with_infima up-complete RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
(T,L) is lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
"\/" ((T,L),T) is Element of the carrier of T
X is Element of the carrier of T
a is Element of the carrier of T
L is Element of the carrier of T
(T,L) is lower Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
"\/" ((T,L),T) is Element of the carrier of T
x is Element of the carrier of T
X is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric upper-bounded with_suprema with_infima up-complete () () RelStr
the carrier of T is non empty set
L is Element of the carrier of T
x is Element of the carrier of T
(T,L) is non empty directed lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
(T,x) is non empty directed lower Element of K10( the carrier of T)
{ b1 where b1 is Element of the carrier of T : (T,b1,x) } is set
"\/" ((T,L),T) is Element of the carrier of T
"\/" ((T,x),T) is Element of the carrier of T
T is non empty V233() reflexive transitive antisymmetric connected RelStr
L is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete connected up-complete /\-complete RelStr
the carrier of L is non empty set
x is Element of the carrier of L
(L,x) is non empty directed filtered lower Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{ b1 where b1 is Element of the carrier of L : (L,b1,x) } is set
"\/" ((L,x),L) is Element of the carrier of L
X is Element of the carrier of L
a is Element of the carrier of L
a is non empty directed filtered Element of K10( the carrier of L)
"\/" (a,L) is Element of the carrier of L
Y is set
y is Element of the carrier of L
T is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of T is non empty set
L is Element of the carrier of T
(T,L) is non empty directed lower Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
{ b1 where b1 is Element of the carrier of T : (T,b1,L) } is set
"\/" ((T,L),T) is Element of the carrier of T
downarrow L is non empty directed lower Element of K10( the carrier of T)
{L} is non empty trivial finite V44(1) countable Element of K10( the carrier of T)
downarrow {L} is non empty lower Element of K10( the carrier of T)
"\/" ((downarrow L),T) is Element of the carrier of T
T is set
the non empty V233() reflexive RelStr is non empty V233() reflexive RelStr
T --> the non empty V233() reflexive RelStr is Relation-like T -defined Function-like constant V31(T) V32(T,{ the non empty V233() reflexive RelStr }) V218() RelStr-yielding Element of K10(K11(T,{ the non empty V233() reflexive RelStr }))
{ the non empty V233() reflexive RelStr } is non empty trivial finite V44(1) countable set
K11(T,{ the non empty V233() reflexive RelStr }) is set
K10(K11(T,{ the non empty V233() reflexive RelStr })) is non empty set
rng (T --> the non empty V233() reflexive RelStr ) is trivial finite countable set
X is Relation-like T -defined Function-like V31(T) set
a is 1-sorted
rng X is set
a is RelStr
rng X is set
T is set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is strict RelStr
the carrier of (product L) is set
Carrier L is Relation-like T -defined Function-like V31(T) set
product (Carrier L) is functional with_common_domain product-like set
rng (Carrier L) is set
dom (Carrier L) is set
x is set
(Carrier L) . x is set
dom L is set
L . x is set
X is 1-sorted
the carrier of X is set
rng L is set
a is non empty RelStr
the carrier of a is non empty set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding set
x is Element of T
L . x is set
dom L is set
L . x is RelStr
rng L is set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
x is Element of T
(T,L,x) is RelStr
dom L is set
rng L is set
X is RelStr
T is set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty strict RelStr
the carrier of (product L) is non empty set
Carrier L is Relation-like T -defined Function-like V31(T) set
product (Carrier L) is functional with_common_domain product-like set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
x is Relation-like Function-like Element of the carrier of (product L)
X is Element of T
x . X is set
(T,L,X) is non empty RelStr
the carrier of (T,L,X) is non empty set
Carrier L is Relation-like T -defined Function-like V31(T) set
(Carrier L) . X is set
product (Carrier L) is functional with_common_domain product-like set
dom (Carrier L) is set
a is 1-sorted
the carrier of a is set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
K10( the carrier of (product L)) is non empty set
x is Element of T
X is Element of K10( the carrier of (product L))
pi (X,x) is set
(T,L,x) is non empty RelStr
the carrier of (T,L,x) is non empty set
K10( the carrier of (T,L,x)) is non empty set
Carrier L is Relation-like T -defined Function-like V31(T) set
product (Carrier L) is functional with_common_domain product-like set
dom (Carrier L) is set
X \/ the carrier of (product L) is non empty set
pi ( the carrier of (product L),x) is set
(pi (X,x)) \/ (pi ( the carrier of (product L),x)) is set
(Carrier L) . x is set
Y is 1-sorted
the carrier of Y is set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
x is Relation-like Function-like set
dom x is set
Carrier L is Relation-like T -defined Function-like V31(T) set
product (Carrier L) is functional with_common_domain product-like set
dom (Carrier L) is set
a is Relation-like Function-like Element of the carrier of (product L)
X is Element of T
(T,L,a,X) is Element of the carrier of (T,L,X)
(T,L,X) is non empty RelStr
the carrier of (T,L,X) is non empty set
x . X is set
X is set
a is Element of T
x . a is set
(T,L,a) is non empty RelStr
the carrier of (T,L,a) is non empty set
(Carrier L) . a is set
x . X is set
(Carrier L) . X is set
Y is 1-sorted
the carrier of Y is set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
X is Relation-like Function-like Element of the carrier of (product L)
a is Relation-like Function-like Element of the carrier of (product L)
Carrier L is Relation-like T -defined Function-like V31(T) set
product (Carrier L) is functional with_common_domain product-like set
Y is Element of T
(T,L,Y) is non empty RelStr
(T,L,X,Y) is Element of the carrier of (T,L,Y)
the carrier of (T,L,Y) is non empty set
(T,L,a,Y) is Element of the carrier of (T,L,Y)
y is Relation-like Function-like set
y is Relation-like Function-like set
y is RelStr
the carrier of y is set
y is Element of the carrier of y
W is Element of the carrier of y
Y is Relation-like Function-like Element of the carrier of (product L)
y is Relation-like Function-like Element of the carrier of (product L)
y is set
L . y is set
Y . y is set
y . y is set
W is Element of T
(T,L,W) is non empty RelStr
the carrier of (T,L,W) is non empty set
(T,L,X,W) is Element of the carrier of (T,L,W)
(T,L,a,W) is Element of the carrier of (T,L,W)
Y is Relation-like Function-like set
y is Relation-like Function-like set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
x is Element of T
(T,L,x) is RelStr
dom L is set
rng L is set
X is RelStr
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
x is Relation-like Function-like Element of the carrier of (product L)
X is Element of T
(T,L,X) is non empty V233() reflexive RelStr
(T,L,x,X) is Element of the carrier of (T,L,X)
the carrier of (T,L,X) is non empty set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
x is Relation-like Function-like Element of the carrier of (product L)
X is Relation-like Function-like Element of the carrier of (product L)
a is Relation-like Function-like Element of the carrier of (product L)
Y is Element of T
(T,L,Y) is non empty RelStr
(T,L,x,Y) is Element of the carrier of (T,L,Y)
the carrier of (T,L,Y) is non empty set
(T,L,X,Y) is Element of the carrier of (T,L,Y)
(T,L,a,Y) is Element of the carrier of (T,L,Y)
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () set
product L is non empty constituted-Functions strict RelStr
the carrier of (product L) is non empty set
x is Relation-like Function-like Element of the carrier of (product L)
X is Relation-like Function-like Element of the carrier of (product L)
dom x is set
dom X is set
a is set
Y is Element of T
(T,L,Y) is non empty RelStr
(T,L,x,Y) is Element of the carrier of (T,L,Y)
the carrier of (T,L,Y) is non empty set
(T,L,X,Y) is Element of the carrier of (T,L,Y)
x . a is set
X . a is set
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () () set
product L is non empty constituted-Functions strict V233() reflexive RelStr
x is Element of T
(T,L,x) is non empty V233() reflexive RelStr
x is Element of T
(T,L,x) is non empty V233() reflexive RelStr
the carrier of (product L) is non empty set
K10( the carrier of (product L)) is non empty set
X is Element of K10( the carrier of (product L))
a is Relation-like T -defined Function-like V31(T) set
dom a is set
Y is Element of T
a . Y is set
(T,L,Y) is non empty V233() reflexive RelStr
(T,L,Y,X) is Element of K10( the carrier of (T,L,Y))
the carrier of (T,L,Y) is non empty set
K10( the carrier of (T,L,Y)) is non empty set
"\/" ((T,L,Y,X),(T,L,Y)) is Element of the carrier of (T,L,Y)
Y is Relation-like Function-like Element of the carrier of (product L)
y is Relation-like Function-like Element of the carrier of (product L)
y is Element of T
(T,L,y,y) is Element of the carrier of (T,L,y)
(T,L,y) is non empty V233() reflexive RelStr
the carrier of (T,L,y) is non empty set
(T,L,y,X) is Element of K10( the carrier of (T,L,y))
K10( the carrier of (T,L,y)) is non empty set
(T,L,Y,y) is Element of the carrier of (T,L,y)
"\/" ((T,L,y,X),(T,L,y)) is Element of the carrier of (T,L,y)
y is Relation-like Function-like Element of the carrier of (product L)
x is non empty V233() reflexive transitive antisymmetric RelStr
y is Element of T
(T,L,Y,y) is Element of the carrier of (T,L,y)
(T,L,y) is non empty V233() reflexive RelStr
the carrier of (T,L,y) is non empty set
(T,L,y,X) is Element of K10( the carrier of (T,L,y))
K10( the carrier of (T,L,y)) is non empty set
"\/" ((T,L,y,X),(T,L,y)) is Element of the carrier of (T,L,y)
(T,L,y,y) is Element of the carrier of (T,L,y)
W is Element of the carrier of (T,L,y)
Z is Relation-like Function-like set
Z . y is set
F is Relation-like Function-like Element of the carrier of (product L)
T is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () () set
product L is non empty constituted-Functions strict V233() reflexive RelStr
the carrier of (product L) is non empty set
K10( the carrier of (product L)) is non empty set
x is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
X is Element of K10( the carrier of (product L))
"\/" (X,(product L)) is Relation-like Function-like Element of the carrier of (product L)
a is Element of T
(T,L,("\/" (X,(product L))),a) is Element of the carrier of (T,L,a)
(T,L,a) is non empty V233() reflexive RelStr
the carrier of (T,L,a) is non empty set
(T,L,a,X) is Element of K10( the carrier of (T,L,a))
K10( the carrier of (T,L,a)) is non empty set
"\/" ((T,L,a,X),(T,L,a)) is Element of the carrier of (T,L,a)
Y is Element of the carrier of (T,L,a)
y is Relation-like Function-like set
y . a is set
y is Relation-like Function-like Element of the carrier of (product L)
Y is Element of the carrier of (T,L,a)
("\/" (X,(product L))) +* (a,Y) is Relation-like Function-like set
dom (("\/" (X,(product L))) +* (a,Y)) is set
dom ("\/" (X,(product L))) is set
y is Element of T
(("\/" (X,(product L))) +* (a,Y)) . y is set
(T,L,("\/" (X,(product L))),y) is Element of the carrier of (T,L,y)
(T,L,y) is non empty V233() reflexive RelStr
the carrier of (T,L,y) is non empty set
y is Relation-like Function-like Element of the carrier of (product L)
W is Relation-like Function-like Element of the carrier of (product L)
(T,L,W,a) is Element of the carrier of (T,L,a)
Z is Element of T
(T,L,y,Z) is Element of the carrier of (T,L,Z)
(T,L,Z) is non empty V233() reflexive RelStr
the carrier of (T,L,Z) is non empty set
(T,L,("\/" (X,(product L))),Z) is Element of the carrier of (T,L,Z)
(T,L,W,Z) is Element of the carrier of (T,L,Z)
(T,L,y,a) is Element of the carrier of (T,L,a)
T is non empty set
K10(T) is non empty set
L is Relation-like T -defined Function-like V31(T) V218() RelStr-yielding () () set
product L is non empty constituted-Functions strict V233() reflexive RelStr
the carrier of (product L) is non empty set
a is Relation-like Function-like Element of the carrier of (product L)
Y is Relation-like Function-like Element of the carrier of (product L)
y is Element of T
(T,L,y) is non empty V233() reflexive RelStr
(T,L,a,y) is Element of the carrier of (T,L,y)
the carrier of (T,L,y) is non empty set
(T,L,Y,y) is Element of the carrier of (T,L,y)
K10( the carrier of (T,L,y)) is non empty set
y is non empty directed Element of K10( the carrier of (T,L,y))
"\/" (y,(T,L,y)) is Element of the carrier of (T,L,y)
dom Y is set
{ (Y +* (y,b1)) where b1 is Element of the carrier of (T,L,y) : b1 in y } is set
Z is set
F is Element of the carrier of (T,L,y)
Y +* (y,F) is Relation-like Function-like set
dom (Y +* (y,F)) is set
ZZ is Element of T
(Y +* (y,F)) . ZZ is set
(T,L,Y,ZZ) is Element of the carrier of (T,L,ZZ)
(T,L,ZZ) is non empty V233() reflexive RelStr
the carrier of (T,L,ZZ) is non empty set
K10( the carrier of (product L)) is non empty set
the Element of y is Element of y
ZZ is Element of the carrier of (T,L,y)
Y +* (y,ZZ) is Relation-like Function-like set
Z is Element of K10( the carrier of (product L))
ZZ is non empty Element of K10( the carrier of (product L))
FZ is Relation-like Function-like Element of the carrier of (product L)
FF is Relation-like Function-like Element of the carrier of (product L)
A is Element of the carrier of (T,L,y)
Y +* (y,A) is Relation-like Function-like set
G is Element of the carrier of (T,L,y)
Y +* (y,G) is Relation-like Function-like set
z is Element of the carrier of (T,L,y)
Y +* (y,z) is Relation-like Function-like set
B is Relation-like Function-like Element of the carrier of (product L)
S is Element of T
(T,L,B,S) is Element of the carrier of (T,L,S)
(T,L,S) is non empty V233() reflexive RelStr
the carrier of (T,L,S) is non empty set
(T,L,FZ,S) is Element of the carrier of (T,L,S)
(T,L,Y,S) is Element of the carrier of (T,L,S)
S is Element of T
(T,L,B,S) is Element of the carrier of (T,L,S)
(T,L,S) is non empty V233() reflexive RelStr
the carrier of (T,L,S) is non empty set
(T,L,FF,S) is Element of the carrier of (T,L,S)
(T,L,Y,S) is Element of the carrier of (T,L,S)
FF is Element of T
(T,L,FF) is non empty V233() reflexive RelStr
FZ is non empty directed Element of K10( the carrier of (product L))
(T,L,y,FZ) is Element of K10( the carrier of (T,L,y))
A is set
G is Element of the carrier of (T,L,y)
Y +* (y,G) is Relation-like Function-like set
(Y +* (y,G)) . y is set
"\/" ((T,L,y,FZ),(T,L,y)) is Element of the carrier of (T,L,y)
"\/" (FZ,(product L)) is Relation-like Function-like Element of the carrier of (product L)
(T,L,("\/" (FZ,(product L))),FF) is Element of the carrier of (T,L,FF)
the carrier of (T,L,FF) is non empty set
(T,L,FF,FZ) is Element of K10( the carrier of (T,L,FF))
K10( the carrier of (T,L,FF)) is non empty set
"\/" ((T,L,FF,FZ),(T,L,FF)) is Element of the carrier of (T,L,FF)
(Y +* (y,ZZ)) . FF is set
(T,L,Y,FF) is Element of the carrier of (T,L,FF)
FF is Relation-like Function-like Element of the carrier of (product L)
A is Element of the carrier of (T,L,y)
Y +* (y,A) is Relation-like Function-like set
(T,L,FF,y) is Element of the carrier of (T,L,y)
{ b1 where b1 is Element of T : not (T,L,a,b1) = Bottom (T,L,b1) } is set
y is set
W is Element of T
(T,L,a,W) is Element of the carrier of (T,L,W)
(T,L,W) is non empty V233() reflexive RelStr
the carrier of (T,L,W) is non empty set
Bottom (T,L,W) is Element of the carrier of (T,L,W)
"\/" ({},(T,L,W)) is Element of the carrier of (T,L,W)
W is Relation-like T -defined Function-like V31(T) set
dom W is set
Z is Element of T
W . Z is set
(T,L,Z) is non empty V233() reflexive RelStr
Bottom (T,L,Z) is Element of the carrier of (T,L,Z)
the carrier of (T,L,Z) is non empty set
"\/" ({},(T,L,Z)) is Element of the carrier of (T,L,Z)
Z is Relation-like Function-like Element of the carrier of (product L)
{ (Z +* (Y | b1)) where b1 is finite countable Element of K10(T) : verum } is set
ZZ is set
ZZ is finite countable Element of K10(T)
Y | ZZ is Relation-like Function-like finite countable set
Z +* (Y | ZZ) is Relation-like Function-like set
dom Y is set
dom (Y | ZZ) is finite countable set
T \/ (dom (Y | ZZ)) is non empty set
dom (Z +* (Y | ZZ)) is set
FZ is Element of T
(Z +* (Y | ZZ)) . FZ is set
(T,L,Z,FZ) is Element of the carrier of (T,L,FZ)
(T,L,FZ) is non empty V233() reflexive RelStr
the carrier of (T,L,FZ) is non empty set
(Y | ZZ) . FZ is set
(T,L,Y,FZ) is Element of the carrier of (T,L,FZ)
K10( the carrier of (product L)) is non empty set
{} T is empty proper Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) V87() countable Element of K10(T)
Y | ({} T) is Relation-like Function-like finite countable set
Z +* (Y | ({} T)) is Relation-like Function-like set
ZZ is Element of K10( the carrier of (product L))
ZZ is non empty Element of K10( the carrier of (product L))
FZ is Relation-like Function-like Element of the carrier of (product L)
FF is Relation-like Function-like Element of the carrier of (product L)
A is finite countable Element of K10(T)
Y | A is Relation-like Function-like finite countable set
Z +* (Y | A) is Relation-like Function-like set
G is finite countable Element of K10(T)
Y | G is Relation-like Function-like finite countable set
Z +* (Y | G) is Relation-like Function-like set
A \/ G is finite countable Element of K10(T)
z is finite countable Element of K10(T)
Y | z is Relation-like Function-like finite countable set
Z +* (Y | z) is Relation-like Function-like set
B is Relation-like Function-like Element of the carrier of (product L)
dom Y is set
dom (Y | z) is finite countable set
dom (Y | A) is finite countable set
dom (Y | G) is finite countable set
S is Element of T
(T,L,S) is non empty V233() reflexive RelStr
Bottom (T,L,S) is Element of the carrier of (T,L,S)
the carrier of (T,L,S) is non empty set
"\/" ({},(T,L,S)) is Element of the carrier of (T,L,S)
(T,L,Y,S) is Element of the carrier of (T,L,S)
(T,L,Z,S) is Element of the carrier of (T,L,S)
(T,L,B,S) is Element of the carrier of (T,L,S)
(Y | z) . S is set
(T,L,FZ,S) is Element of the carrier of (T,L,S)
(T,L,B,S) is Element of the carrier of (T,L,S)
(T,L,FZ,S) is Element of the carrier of (T,L,S)
(T,L,B,S) is Element of the carrier of (T,L,S)
(Y | z) . S is set
(T,L,FZ,S) is Element of the carrier of (T,L,S)
(Y | A) . S is set
S is Element of T
(T,L,S) is non empty V233() reflexive RelStr
Bottom (T,L,S) is Element of the carrier of (T,L,S)
the carrier of (T,L,S) is non empty set
"\/" ({},(T,L,S)) is Element of the carrier of (T,L,S)
(T,L,Y,S) is Element of the carrier of (T,L,S)
(T,L,Z,S) is Element of the carrier of (T,L,S)
(T,L,B,S) is Element of the carrier of (T,L,S)
(Y | z) . S is set
(T,L,FF,S) is Element of the carrier of (T,L,S)
(T,L,B,S) is Element of the carrier of (T,L,S)
(T,L,FF,S) is Element of the carrier of (T,L,S)
(T,L,B,S) is Element of the carrier of (T,L,S)
(Y | z) . S is set
(T,L,FF,S) is Element of the carrier of (T,L,S)
(Y | G) . S is set
FF is Element of T
{FF} is non empty trivial finite V44(1) countable Element of K10(T)
A is finite countable Element of K10(T)
Y | A is Relation-like Function-like finite countable set
Z +* (Y | A) is Relation-like Function-like set
FZ is non empty directed Element of K10( the carrier of (product L))
X is non empty V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
dom Y is set
(Y | A) . FF is set
(T,L,Y,FF) is Element of the carrier of (T,L,FF)
(T,L,FF) is non empty V233() reflexive RelStr
the carrier of (T,L,FF) is non empty set
dom (Y | A) is finite countable set
G is Relation-like Function-like Element of the carrier of (product L)
"\/" (FZ,(product L)) is Relation-like Function-like Element of the carrier of (product L)
(T,L,G,FF) is Element of the carrier of (T,L,FF)
(T,L,("\/" (FZ,(product L))),FF) is Element of the carrier of (T,L,FF)
FF is Relation-like Function-like Element of the carrier of (product L)
A is finite countable Element of K10(T)
Y | A is Relation-like Function-like finite countable set
Z +* (Y | A) is Relation-like Function-like set
y is Element of K10(T)
G is set
z is Element of T
(T,L,a,z) is Element of the carrier of (T,L,z)
(T,L,z) is non empty V233() reflexive RelStr
the carrier of (T,L,z) is non empty set
Bottom (T,L,z) is Element of the carrier of (T,L,z)
"\/" ({},(T,L,z)) is Element of the carrier of (T,L,z)
dom (Y | A) is finite countable set
(T,L,FF,z) is Element of the carrier of (T,L,z)
(T,L,Z,z) is Element of the carrier of (T,L,z)
G is finite countable Element of K10(T)
z is finite countable Element of K10(T)
B is Element of T
(T,L,a,B) is Element of the carrier of (T,L,B)
(T,L,B) is non empty V233() reflexive RelStr
the carrier of (T,L,B) is non empty set
Bottom (T,L,B) is Element of the carrier of (T,L,B)
"\/" ({},(T,L,B)) is Element of the carrier of (T,L,B)
y is finite countable Element of K10(T)
y is non empty directed Element of K10( the carrier of (product L))
"\/" (y,(product L)) is Relation-like Function-like Element of the carrier of (product L)
W is set
Z is Element of T
(T,L,Z) is non empty V233() reflexive RelStr
(T,L,Z,y) is Element of K10( the carrier of (T,L,Z))
the carrier of (T,L,Z) is non empty set
K10( the carrier of (T,L,Z)) is non empty set
F is Element of the carrier of (T,L,Z)
ZZ is Element of the carrier of (T,L,Z)
ZZ is Relation-like Function-like set
ZZ . Z is set
FZ is Relation-like Function-like set
FZ . Z is set
FF is Relation-like Function-like Element of the carrier of (product L)
A is Relation-like Function-like Element of the carrier of (product L)
G is Relation-like Function-like Element of the carrier of (product L)
(T,L,G,Z) is Element of the carrier of (T,L,Z)
the Element of y is Element of y
ZZ is Relation-like Function-like Element of the carrier of (product L)
(T,L,ZZ,Z) is Element of the carrier of (T,L,Z)
(T,L,a,Z) is Element of the carrier of (T,L,Z)
(T,L,Y,Z) is Element of the carrier of (T,L,Z)
(T,L,("\/" (y,(product L))),Z) is Element of the carrier of (T,L,Z)
"\/" ((T,L,Z,y),(T,L,Z)) is Element of the carrier of (T,L,Z)
ZZ is Element of the carrier of (T,L,Z)
FZ is Relation-like Function-like set
FZ . Z is set
FF is set
A is set
W is Relation-like Function-like set
dom W is set
rng W is set
K10(y) is non empty set
Z is finite countable Element of K10(y)
F is Relation-like Function-like Element of the carrier of (product L)
ZZ is Element of T
(T,L,ZZ) is non empty V233() reflexive RelStr
W . ZZ is set
ZZ is Element of T
FZ is Relation-like Function-like Element of the carrier of (product L)
(T,L,ZZ) is non empty V233() reflexive RelStr
(T,L,a,ZZ) is Element of the carrier of (T,L,ZZ)
the carrier of (T,L,ZZ) is non empty set
(T,L,FZ,ZZ) is Element of the carrier of (T,L,ZZ)
(T,L,FZ,ZZ) is Element of the carrier of (T,L,ZZ)
the carrier of (T,L,ZZ) is non empty set
(T,L,F,ZZ) is Element of the carrier of (T,L,ZZ)
(T,L,a,ZZ) is Element of the carrier of (T,L,ZZ)
(T,L,a,ZZ) is Element of the carrier of (T,L,ZZ)
the carrier of (T,L,ZZ) is non empty set
Bottom (T,L,ZZ) is Element of the carrier of (T,L,ZZ)
"\/" ({},(T,L,ZZ)) is Element of the carrier of (T,L,ZZ)
(T,L,F,ZZ) is Element of the carrier of (T,L,ZZ)
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
x is Element of the carrier of (InclPoset the topology of T)
X is Element of the carrier of (InclPoset the topology of T)
a is Element of K10(K10( the carrier of T))
union a is Element of K10( the carrier of T)
K10(a) is non empty set
K10( the carrier of (InclPoset the topology of T)) is non empty set
Y is Element of K10( the carrier of (InclPoset the topology of T))
"\/" (Y,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
y is finite countable Element of K10( the carrier of (InclPoset the topology of T))
"\/" (y,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
y is finite countable Element of K10(a)
union y is set
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
RelIncl the topology of T is V31( the topology of T) V221() V224() V228() Element of K10(K11( the topology of T, the topology of T))
K11( the topology of T, the topology of T) is non empty set
K10(K11( the topology of T, the topology of T)) is non empty set
RelStr(# the topology of T,(RelIncl the topology of T) #) is non empty strict V233() reflexive transitive antisymmetric RelStr
X is Element of the carrier of (InclPoset the topology of T)
x is Element of the carrier of (InclPoset the topology of T)
K10( the carrier of (InclPoset the topology of T)) is non empty set
a is non empty directed lower Element of K10( the carrier of (InclPoset the topology of T))
"\/" (a,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
Y is Element of K10(K10( the carrier of T))
union Y is Element of K10( the carrier of T)
K10(Y) is non empty set
y is finite countable Element of K10(Y)
union y is set
y is finite countable Element of K10( the carrier of (InclPoset the topology of T))
W is Element of the carrier of (InclPoset the topology of T)
union y is set
"\/" (y,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
L is Element of the carrier of (InclPoset the topology of T)
x is Element of K10( the carrier of T)
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
K10(X) is non empty set
a is finite countable Element of K10(X)
union a is set
Y is Element of K10(K10( the carrier of T))
union Y is Element of K10( the carrier of T)
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
a is Element of K10(K10( the carrier of T))
union a is Element of K10( the carrier of T)
K10(X) is non empty set
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
L is Element of the carrier of (InclPoset the topology of T)
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
L is Element of the carrier of T
x is Element of K10( the carrier of T)
X is open Element of K10( the carrier of T)
Cl X is closed Element of K10( the carrier of T)
a is closed Element of K10( the carrier of T)
Int a is open Element of K10( the carrier of T)
0 is empty Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) V87() countable Element of NAT
{0} is non empty trivial finite V41() V44(1) countable Element of K10(NAT)
1TopSp {0} is non empty finite strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 compact () TopStruct
bool {0} is non empty finite V41() countable Element of K10(K10({0}))
K10({0}) is non empty finite V41() countable set
K10(K10({0})) is non empty finite V41() countable set
[#] (bool {0}) is non empty non proper finite V41() countable Element of K10((bool {0}))
K10((bool {0})) is non empty finite V41() countable set
TopStruct(# {0},([#] (bool {0})) #) is non empty strict TopStruct
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
x is Element of the carrier of (InclPoset the topology of T)
X is Element of the carrier of (InclPoset the topology of T)
a is Element of K10( the carrier of T)
RelIncl the topology of T is V31( the topology of T) V221() V224() V228() Element of K10(K11( the topology of T, the topology of T))
K11( the topology of T, the topology of T) is non empty set
K10(K11( the topology of T, the topology of T)) is non empty set
RelStr(# the topology of T,(RelIncl the topology of T) #) is non empty strict V233() reflexive transitive antisymmetric RelStr
K10( the carrier of (InclPoset the topology of T)) is non empty set
y is non empty directed Element of K10( the carrier of (InclPoset the topology of T))
"\/" (y,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
union y is set
W is Element of K10(K10( the carrier of T))
Z is Element of K10(K10( the carrier of T))
F is Element of K10( the carrier of T)
y is Element of K10( the carrier of T)
union Z is Element of K10( the carrier of T)
F is Element of K10(K10( the carrier of T))
ZZ is Element of the carrier of (InclPoset the topology of T)
ZZ is set
FZ is Element of the carrier of (InclPoset the topology of T)
union F is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
RelIncl the topology of T is V31( the topology of T) V221() V224() V228() Element of K10(K11( the topology of T, the topology of T))
K11( the topology of T, the topology of T) is non empty set
K10(K11( the topology of T, the topology of T)) is non empty set
RelStr(# the topology of T,(RelIncl the topology of T) #) is non empty strict V233() reflexive transitive antisymmetric RelStr
x is Element of the carrier of (InclPoset the topology of T)
X is Element of the carrier of (InclPoset the topology of T)
Y is Element of K10( the carrier of T)
{ (Int b1) where b1 is Element of K10( the carrier of T) : ( b1 c= Y & b1 is compact ) } is set
{} T is empty proper Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) open closed boundary nowhere_dense compact V87() countable Element of K10( the carrier of T)
Int ({} T) is empty proper Function-like functional ext-real V23() V24() V25() V27() V28() V29() V30() finite V41() V42() V44( {} ) open closed boundary nowhere_dense compact V87() countable Element of K10( the carrier of T)
y is Element of K10( the carrier of T)
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
W is set
Z is Element of K10( the carrier of T)
Int Z is open Element of K10( the carrier of T)
W is non empty Element of K10(K10( the carrier of T))
union W is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
ZZ is Element of K10( the carrier of T)
Int ZZ is open Element of K10( the carrier of T)
K10( the carrier of (InclPoset the topology of T)) is non empty set
F is Element of K10( the carrier of (InclPoset the topology of T))
"\/" (F,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
ZZ is set
ZZ is Element of the carrier of T
FZ is Element of K10( the carrier of T)
Int FZ is open Element of K10( the carrier of T)
ZZ is finite countable Element of K10( the carrier of (InclPoset the topology of T))
"\/" (ZZ,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
ZZ is set
FZ is Element of K10( the carrier of T)
Int FZ is open Element of K10( the carrier of T)
FF is set
A is set
ZZ is Relation-like Function-like set
dom ZZ is set
FZ is Element of K10(K10( the carrier of T))
union FZ is Element of K10( the carrier of T)
a is Element of K10( the carrier of T)
FF is set
rng ZZ is set
A is set
ZZ . A is set
G is Element of K10( the carrier of T)
Int G is open Element of K10( the carrier of T)
union (rng ZZ) is set
FF is Element of K10( the carrier of T)
A is set
G is set
ZZ . G is set
z is Element of K10( the carrier of T)
Int z is open Element of K10( the carrier of T)
A is set
G is set
z is set
ZZ . z is set
B is Element of K10( the carrier of T)
Int B is open Element of K10( the carrier of T)
A is set
G is set
union G is set
z is Element of K10( the carrier of T)
z is Element of K10( the carrier of T)
{A} is non empty trivial finite V44(1) countable set
G \/ {A} is non empty set
union (G \/ {A}) is set
B is set
ZZ . B is set
S is Element of K10( the carrier of T)
Int S is open Element of K10( the carrier of T)
z \/ S is Element of K10( the carrier of T)
Bx is Element of K10( the carrier of T)
union {A} is set
(union G) \/ (union {A}) is set
A is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
RelIncl the topology of T is V31( the topology of T) V221() V224() V228() Element of K10(K11( the topology of T, the topology of T))
K11( the topology of T, the topology of T) is non empty set
K10(K11( the topology of T, the topology of T)) is non empty set
RelStr(# the topology of T,(RelIncl the topology of T) #) is non empty strict V233() reflexive transitive antisymmetric RelStr
x is Element of the carrier of (InclPoset the topology of T)
X is Element of the carrier of (InclPoset the topology of T)
a is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
Cl Y is closed Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
RelIncl the topology of T is V31( the topology of T) V221() V224() V228() Element of K10(K11( the topology of T, the topology of T))
K11( the topology of T, the topology of T) is non empty set
K10(K11( the topology of T, the topology of T)) is non empty set
RelStr(# the topology of T,(RelIncl the topology of T) #) is non empty strict V233() reflexive transitive antisymmetric RelStr
x is Element of the carrier of T
X is Element of K10( the carrier of T)
the carrier of (InclPoset the topology of T) is non empty non trivial set
a is Element of the carrier of (InclPoset the topology of T)
((InclPoset the topology of T),a) is non empty directed lower Element of K10( the carrier of (InclPoset the topology of T))
K10( the carrier of (InclPoset the topology of T)) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of T) : ( InclPoset the topology of T,b1,a) } is set
"\/" (((InclPoset the topology of T),a),(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
union ((InclPoset the topology of T),a) is set
Y is set
y is Element of K10( the carrier of T)
y is Element of the carrier of (InclPoset the topology of T)
W is open Element of K10( the carrier of T)
Cl W is closed Element of K10( the carrier of T)
Z is closed Element of K10( the carrier of T)
Int Z is open Element of K10( the carrier of T)
F is Element of K10(K10( the carrier of T))
Z ` is open Element of K10( the carrier of T)
the carrier of T \ Z is set
{(Z `)} is non empty trivial finite V44(1) countable Element of K10(K10( the carrier of T))
ZZ is Element of K10(K10( the carrier of T))
ZZ is Element of K10(K10( the carrier of T))
F \/ ZZ is Element of K10(K10( the carrier of T))
FF is Element of K10( the carrier of T)
FZ is Element of K10(K10( the carrier of T))
FF is Element of K10( the carrier of (InclPoset the topology of T))
"\/" (FF,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
union FZ is Element of K10( the carrier of T)
union F is Element of K10( the carrier of T)
union ZZ is Element of K10( the carrier of T)
(union F) \/ (union ZZ) is Element of K10( the carrier of T)
(union F) \/ (Z `) is Element of K10( the carrier of T)
Z \/ (Z `) is Element of K10( the carrier of T)
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
A is finite countable Element of K10( the carrier of (InclPoset the topology of T))
"\/" (A,(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
union A is set
A \ ZZ is finite countable Element of K10( the carrier of (InclPoset the topology of T))
G is Element of K10(K10( the carrier of T))
union G is Element of K10( the carrier of T)
z is set
B is set
T is non empty TopSpace-like TopStruct
the topology of T is non empty open Element of K10(K10( the carrier of T))
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict V233() reflexive transitive antisymmetric lower-bounded upper-bounded V240() with_suprema with_infima complete up-complete /\-complete RelStr
RelIncl the topology of T is V31( the topology of T) V221() V224() V228() Element of K10(K11( the topology of T, the topology of T))
K11( the topology of T, the topology of T) is non empty set
K10(K11( the topology of T, the topology of T)) is non empty set
RelStr(# the topology of T,(RelIncl the topology of T) #) is non empty strict V233() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
x is Element of the carrier of (InclPoset the topology of T)
((InclPoset the topology of T),x) is non empty directed lower Element of K10( the carrier of (InclPoset the topology of T))
K10( the carrier of (InclPoset the topology of T)) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of T) : ( InclPoset the topology of T,b1,x) } is set
X is Element of the carrier of (InclPoset the topology of T)
((InclPoset the topology of T),X) is non empty directed lower Element of K10( the carrier of (InclPoset the topology of T))
{ b1 where b1 is Element of the carrier of (InclPoset the topology of T) : ( InclPoset the topology of T,b1,X) } is set
x is Element of the carrier of (InclPoset the topology of T)
((InclPoset the topology of T),x) is non empty directed lower Element of K10( the carrier of (InclPoset the topology of T))
K10( the carrier of (InclPoset the topology of T)) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of T) : ( InclPoset the topology of T,b1,x) } is set
"\/" (((InclPoset the topology of T),x),(InclPoset the topology of T)) is Element of the carrier of (InclPoset the topology of T)
a is set
X is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
Int Y is open Element of K10( the carrier of T)
y is Element of K10( the carrier of T)
y is Element of the carrier of (InclPoset the topology of T)
union ((InclPoset the topology of T),x) is set
a is set
union ((InclPoset the topology of T),x) is set
Y is set
y is Element of the carrier of (InclPoset the topology of T)