:: WAYBEL_3 semantic presentation

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

{ b

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

{ b

x is set

X is Element of the carrier of T

K10( the carrier of T) is non empty set

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

(T,x) is Element of K10( the carrier of T)

{ b

(T,x) is Element of K10( the carrier of T)

{ b

(T,L) is Element of K10( the carrier of T)

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

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

{ ("\/" (b

"\/" (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 "/\" b

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,b

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

{ b

"\/" ((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

{ b

x is Element of the carrier of T

(T,x) is non empty directed lower Element of K10( the carrier of T)

{ b

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

{ b

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

{ b

"\/" ((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)

{ b

"\/" ((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

{ b

(T,x) is non empty directed lower Element of K10( the carrier of T)

{ b

"\/" ((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

{ b

"\/" ((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

{ b

"\/" ((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,b

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)

{ b

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

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 b

{} 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

{ b

"\/" (((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

{ b

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

{ b

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

{ b

"\/" (((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)