:: WAYBEL23 semantic presentation

K170() is non trivial ordinal non finite cardinal limit_cardinal Element of K32(K166())

K166() is set

K32(K166()) is non empty set

omega is non trivial ordinal non finite cardinal limit_cardinal set

K32(omega) is non empty non trivial non finite set

{} is set

the empty ordinal natural finite V32() cardinal {} -element set is empty ordinal natural finite V32() cardinal {} -element set

1 is non empty set

{{},1} is finite set

K32(K170()) is non empty non trivial non finite set

T is non empty reflexive transitive antisymmetric RelStr

the carrier of T is non empty set

CompactSublatt T is strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (CompactSublatt T) is set

X is Element of the carrier of T

compactbelow X is Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

waybelow X is lower Element of K32( the carrier of T)

(waybelow X) /\ the carrier of (CompactSublatt T) is Element of K32( the carrier of T)

A is set

downarrow X is non empty directed lower Element of K32( the carrier of T)

(downarrow X) /\ the carrier of (CompactSublatt T) is Element of K32( the carrier of T)

b is Element of the carrier of T

A is set

b is Element of the carrier of T

downarrow X is non empty directed lower Element of K32( the carrier of T)

(downarrow X) /\ the carrier of (CompactSublatt T) is Element of K32( the carrier of T)

T is non empty reflexive transitive RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

K32( the carrier of (InclPoset (Ids T))) is non empty set

X is Element of K32( the carrier of (InclPoset (Ids T)))

union X is set

the carrier of T is non empty set

K32( the carrier of T) is non empty set

A is set

b is set

c

T is non empty set

InclPoset T is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset T) is non empty set

K32( the carrier of (InclPoset T)) is non empty set

X is Element of K32( the carrier of (InclPoset T))

union X is set

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

A is set

b is Element of the carrier of (InclPoset T)

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

A is Element of K32( the carrier of T)

finsups X is Element of K32( the carrier of T)

finsups A is Element of K32( the carrier of T)

b is set

K32(X) is non empty set

{ ("\/" (b

c

"\/" (c

K32(A) is non empty set

y is finite Element of K32(A)

{ ("\/" (b

T is non empty transitive RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty transitive full join-inheriting sups-inheriting directed-sups-inheriting SubRelStr of T

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is Element of K32( the carrier of T)

finsups A is Element of K32( the carrier of T)

b is Element of K32( the carrier of X)

finsups b is Element of K32( the carrier of X)

c

K32(A) is non empty set

{ ("\/" (b

y is finite Element of K32(A)

"\/" (y,T) is Element of the carrier of T

K32(b) is non empty set

y1 is finite Element of K32(b)

C is Element of K32( the carrier of X)

"\/" (C,T) is Element of the carrier of T

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

{ ("\/" (b

T is non empty transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty transitive antisymmetric full join-inheriting sups-inheriting with_suprema directed-sups-inheriting SubRelStr of T

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is Element of K32( the carrier of T)

finsups A is non empty Element of K32( the carrier of T)

b is Element of K32( the carrier of X)

finsups b is Element of K32( the carrier of X)

c

K32(b) is non empty set

{ ("\/" (b

y is finite Element of K32(b)

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

K32(A) is non empty set

y1 is finite Element of K32(A)

C is Element of K32( the carrier of X)

"\/" (C,T) is Element of the carrier of T

{ ("\/" (b

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete 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

K32( the carrier of T) is non empty set

X is non empty reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of T

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is Element of K32( the carrier of T)

finsups A is non empty directed Element of K32( the carrier of T)

b is Element of K32( the carrier of X)

finsups b is directed Element of K32( the carrier of X)

c

K32(b) is non empty set

{ ("\/" (b

y is finite Element of K32(b)

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

K32(A) is non empty set

y1 is finite Element of K32(A)

C is non empty finite Element of K32( the carrier of X)

"\/" (C,T) is Element of the carrier of T

a1 is Element of the carrier of X

a2 is Element of the carrier of T

d1 is Element of the carrier of T

d2 is Element of the carrier of X

a is Element of the carrier of X

a1 is Element of the carrier of X

a2 is Element of the carrier of T

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

{ ("\/" (b

y1 is finite Element of K32(A)

Bottom X is Element of the carrier of X

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

C is Element of the carrier of X

a is Element of the carrier of T

{ ("\/" (b

y1 is finite Element of K32(A)

T is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

the carrier of (InclPoset (Ids T)) is non empty set

K32( the carrier of (InclPoset (Ids T))) is non empty set

X is Element of K32( the carrier of (InclPoset (Ids T)))

"\/" (X,(InclPoset (Ids T))) is Element of the carrier of (InclPoset (Ids T))

(T,X) is Element of K32( the carrier of T)

the carrier of T is non empty set

K32( the carrier of T) is non empty set

finsups (T,X) is non empty directed Element of K32( the carrier of T)

downarrow (finsups (T,X)) is non empty directed lower Element of K32( the carrier of T)

b is Element of the carrier of (InclPoset (Ids T))

c

A is Element of the carrier of (InclPoset (Ids T))

b is Element of the carrier of (InclPoset (Ids T))

T is reflexive transitive RelStr

the carrier of T is set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

downarrow X is Element of K32( the carrier of T)

downarrow (downarrow X) is Element of K32( the carrier of T)

A is set

b is Element of the carrier of T

c

y is Element of the carrier of T

T is reflexive transitive RelStr

the carrier of T is set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

uparrow X is Element of K32( the carrier of T)

uparrow (uparrow X) is Element of K32( the carrier of T)

A is set

b is Element of the carrier of T

c

y is Element of the carrier of T

T is non empty reflexive transitive RelStr

the carrier of T is non empty set

X is Element of the carrier of T

downarrow X is non empty directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

downarrow (downarrow X) is non empty directed lower Element of K32( the carrier of T)

A is set

b is Element of the carrier of T

c

T is non empty reflexive transitive RelStr

the carrier of T is non empty set

X is Element of the carrier of T

uparrow X is non empty filtered upper Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

uparrow (uparrow X) is non empty filtered upper Element of K32( the carrier of T)

A is set

b is Element of the carrier of T

c

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty SubRelStr of T

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is Element of K32( the carrier of T)

downarrow A is Element of K32( the carrier of T)

b is Element of K32( the carrier of X)

downarrow b is Element of K32( the carrier of X)

c

y is Element of the carrier of X

y1 is Element of the carrier of X

C is Element of the carrier of T

a is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty SubRelStr of T

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is Element of K32( the carrier of T)

uparrow A is Element of K32( the carrier of T)

b is Element of K32( the carrier of X)

uparrow b is Element of K32( the carrier of X)

c

y is Element of the carrier of X

y1 is Element of the carrier of X

a is Element of the carrier of T

C is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

X is non empty SubRelStr of T

the carrier of X is non empty set

A is Element of the carrier of T

downarrow A is Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is Element of the carrier of X

downarrow b is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

{A} is non empty trivial finite 1 -element Element of K32( the carrier of T)

downarrow {A} is Element of K32( the carrier of T)

{b} is non empty trivial finite 1 -element Element of K32( the carrier of X)

downarrow {b} is Element of K32( the carrier of X)

T is non empty RelStr

the carrier of T is non empty set

X is non empty SubRelStr of T

the carrier of X is non empty set

A is Element of the carrier of T

uparrow A is Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is Element of the carrier of X

uparrow b is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

{A} is non empty trivial finite 1 -element Element of K32( the carrier of T)

uparrow {A} is Element of K32( the carrier of T)

{b} is non empty trivial finite 1 -element Element of K32( the carrier of X)

uparrow {b} is Element of K32( the carrier of X)

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict full SubRelStr of T

A is meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of T

X is Element of K32( the carrier of T)

subrelstr X is strict full SubRelStr of T

A is join-inheriting sups-inheriting directed-sups-inheriting SubRelStr of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict full SubRelStr of T

the carrier of (subrelstr X) is set

K32( the carrier of (subrelstr X)) is non empty set

A is Element of K32( the carrier of (subrelstr X))

"/\" (A,T) is Element of the carrier of T

A is Element of K32( the carrier of (subrelstr X))

"\/" (A,T) is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict full SubRelStr of T

A is Element of the carrier of T

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"/\" ({A,b},T) is Element of the carrier of T

the carrier of (subrelstr X) is set

A is Element of the carrier of T

subrelstr X is strict full SubRelStr of T

the carrier of (subrelstr X) is set

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"/\" ({A,b},T) is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict full SubRelStr of T

A is Element of the carrier of T

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"\/" ({A,b},T) is Element of the carrier of T

the carrier of (subrelstr X) is set

A is Element of the carrier of T

subrelstr X is strict full SubRelStr of T

the carrier of (subrelstr X) is set

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"\/" ({A,b},T) is Element of the carrier of T

T is non empty antisymmetric with_infima RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

A is Element of the carrier of T

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"/\" ({A,b},T) is Element of the carrier of T

A is Element of the carrier of T

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"/\" ({A,b},T) is Element of the carrier of T

T is non empty antisymmetric with_suprema RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

A is Element of the carrier of T

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"\/" ({A,b},T) is Element of the carrier of T

A is Element of the carrier of T

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

"\/" ({A,b},T) is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

K32(X) is non empty set

subrelstr X is strict full SubRelStr of T

A is Element of K32(X)

"/\" (A,T) is Element of the carrier of T

the carrier of (subrelstr X) is set

K32( the carrier of (subrelstr X)) is non empty set

subrelstr X is strict full SubRelStr of T

the carrier of (subrelstr X) is set

K32( the carrier of (subrelstr X)) is non empty set

A is Element of K32( the carrier of (subrelstr X))

"/\" (A,T) is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

K32(X) is non empty set

subrelstr X is strict full SubRelStr of T

A is Element of K32(X)

"\/" (A,T) is Element of the carrier of T

the carrier of (subrelstr X) is set

K32( the carrier of (subrelstr X)) is non empty set

subrelstr X is strict full SubRelStr of T

the carrier of (subrelstr X) is set

K32( the carrier of (subrelstr X)) is non empty set

A is Element of K32( the carrier of (subrelstr X))

"\/" (A,T) is Element of the carrier of T

T is non empty transitive RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) (T) Element of K32( the carrier of T)

K32(X) is non empty set

subrelstr X is non empty strict transitive full SubRelStr of T

A is Element of K32(X)

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

the carrier of (subrelstr X) is non empty set

"/\" (A,T) is Element of the carrier of T

K32( the carrier of (subrelstr X)) is non empty set

T is non empty transitive RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) (T) Element of K32( the carrier of T)

K32(X) is non empty set

subrelstr X is non empty strict transitive full SubRelStr of T

A is Element of K32(X)

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

the carrier of (subrelstr X) is non empty set

"\/" (A,T) is Element of the carrier of T

K32( the carrier of (subrelstr X)) is non empty set

T is non empty transitive RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict transitive full SubRelStr of T

A is Element of X

b is Element of X

{A,b} is finite Element of K32(X)

K32(X) is non empty set

"/\" ({A,b},(subrelstr X)) is Element of the carrier of (subrelstr X)

the carrier of (subrelstr X) is non empty set

"/\" ({A,b},T) is Element of the carrier of T

T is non empty transitive RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict transitive full SubRelStr of T

A is Element of X

b is Element of X

{A,b} is finite Element of K32(X)

K32(X) is non empty set

"\/" ({A,b},(subrelstr X)) is Element of the carrier of (subrelstr X)

the carrier of (subrelstr X) is non empty set

"\/" ({A,b},T) is Element of the carrier of T

T is non empty transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict transitive antisymmetric full SubRelStr of T

T is non empty transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict transitive antisymmetric full SubRelStr of T

T is non empty transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict transitive antisymmetric full SubRelStr of T

T is non empty transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict transitive antisymmetric full SubRelStr of T

T is non empty transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) (T) Element of K32( the carrier of T)

K32(X) is non empty set

subrelstr X is non empty strict transitive antisymmetric full with_infima SubRelStr of T

A is Element of K32(X)

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

the carrier of (subrelstr X) is non empty set

"/\" (A,T) is Element of the carrier of T

T is non empty transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) (T) Element of K32( the carrier of T)

K32(X) is non empty set

subrelstr X is non empty strict transitive antisymmetric full with_suprema SubRelStr of T

A is Element of K32(X)

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

the carrier of (subrelstr X) is non empty set

"\/" (A,T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is (T) Element of K32( the carrier of T)

subrelstr X is strict reflexive transitive antisymmetric full SubRelStr of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is (T) Element of K32( the carrier of T)

subrelstr X is strict reflexive transitive antisymmetric full SubRelStr of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty upper Element of K32( the carrier of T)

subrelstr X is non empty strict reflexive transitive antisymmetric full SubRelStr of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty lower Element of K32( the carrier of T)

subrelstr X is non empty strict reflexive transitive antisymmetric full SubRelStr of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is (T) Element of K32( the carrier of T)

A is (T) Element of K32( the carrier of T)

X /\ A is Element of K32( the carrier of T)

subrelstr A is strict full SubRelStr of T

subrelstr X is strict full SubRelStr of T

b is Element of the carrier of T

subrelstr (X /\ A) is strict full SubRelStr of T

the carrier of (subrelstr (X /\ A)) is set

c

{b,c

the carrier of (subrelstr A) is set

"\/" ({b,c

the carrier of (subrelstr X) is set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is (T) Element of K32( the carrier of T)

A is (T) Element of K32( the carrier of T)

X /\ A is Element of K32( the carrier of T)

subrelstr A is strict full SubRelStr of T

subrelstr X is strict full SubRelStr of T

b is Element of the carrier of T

subrelstr (X /\ A) is strict full SubRelStr of T

the carrier of (subrelstr (X /\ A)) is set

c

{b,c

the carrier of (subrelstr A) is set

"/\" ({b,c

the carrier of (subrelstr X) is set

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

X is Element of the carrier of T

downarrow X is non empty directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is Element of the carrier of T

subrelstr (downarrow X) is non empty strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (downarrow X)) is non empty set

c

{b,c

A is Element of the carrier of T

b "\/" c

"\/" ({b,c

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

X is Element of the carrier of T

downarrow X is non empty directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is Element of the carrier of T

subrelstr (downarrow X) is non empty strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (downarrow X)) is non empty set

c

{b,c

A is Element of the carrier of T

b "/\" c

"/\" ({b,c

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

X is Element of the carrier of T

uparrow X is non empty filtered upper Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is Element of the carrier of T

subrelstr (uparrow X) is non empty strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (uparrow X)) is non empty set

c

{b,c

A is Element of the carrier of T

b "\/" c

"\/" ({b,c

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

X is Element of the carrier of T

uparrow X is non empty filtered upper Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is Element of the carrier of T

subrelstr (uparrow X) is non empty strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (uparrow X)) is non empty set

c

{b,c

A is Element of the carrier of T

A "/\" A is Element of the carrier of T

b "/\" c

"/\" ({b,c

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

X is Element of the carrier of T

downarrow X is non empty directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

uparrow X is non empty filtered upper Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

X is Element of the carrier of T

downarrow X is non empty directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

uparrow X is non empty filtered upper Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

X is Element of the carrier of T

waybelow X is directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

A is Element of the carrier of T

subrelstr (waybelow X) is strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (waybelow X)) is set

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

A "\/" b is Element of the carrier of T

"\/" ({A,b},T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

X is Element of the carrier of T

waybelow X is lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

A is Element of the carrier of T

subrelstr (waybelow X) is strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (waybelow X)) is set

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

A "/\" b is Element of the carrier of T

"/\" ({A,b},T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

X is Element of the carrier of T

wayabove X is upper Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

A is Element of the carrier of T

subrelstr (wayabove X) is strict reflexive transitive antisymmetric full SubRelStr of T

the carrier of (subrelstr (wayabove X)) is set

b is Element of the carrier of T

{A,b} is finite Element of K32( the carrier of T)

A "\/" b is Element of the carrier of T

"\/" ({A,b},T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

X is Element of the carrier of T

waybelow X is directed lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

wayabove X is upper Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

X is Element of the carrier of T

waybelow X is lower Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

T is TopStruct

the carrier of T is set

K32( the carrier of T) is non empty set

K32(K32( the carrier of T)) is non empty set

{ (card b

meet { (card b

the topology of T is Element of K32(K32( the carrier of T))

card the topology of T is ordinal cardinal set

A is ordinal set

c

card c

c

b is ordinal cardinal set

y is set

C is V63(T) V231(T) Element of K32(K32( the carrier of T))

card C is ordinal cardinal set

y1 is ordinal cardinal set

the topology of T is Element of K32(K32( the carrier of T))

card the topology of T is ordinal cardinal set

T is non empty reflexive transitive antisymmetric upper-bounded with_suprema up-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

[#] T is non empty non proper directed lower upper Element of K32( the carrier of T)

X is non empty non proper directed lower upper Element of K32( the carrier of T)

subrelstr X is non empty strict reflexive transitive antisymmetric full SubRelStr of T

A is Element of the carrier of T

waybelow A is non empty directed lower (T) Element of K32( the carrier of T)

(waybelow A) /\ X is Element of K32( the carrier of T)

"\/" (((waybelow A) /\ X),T) is Element of the carrier of T

"\/" ((waybelow A),T) is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

T is non empty RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

[#] T is non empty non proper lower upper Element of K32( the carrier of T)

Bottom T is Element of the carrier of T

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

[#] T is non empty non proper lower upper Element of K32( the carrier of T)

Top T is Element of the carrier of T

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

T is non empty reflexive transitive antisymmetric upper-bounded with_suprema up-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

X is Element of the carrier of T

waybelow X is non empty directed lower (T) Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

[#] T is non empty non proper directed lower upper Element of K32( the carrier of T)

(waybelow X) /\ ([#] T) is Element of K32( the carrier of T)

"\/" (((waybelow X) /\ ([#] T)),T) is Element of the carrier of T

X is Element of the carrier of T

A is Element of the carrier of T

{X,A} is finite Element of K32( the carrier of T)

"\/" ({X,A},T) is Element of the carrier of T

X is (T)

Bottom T is Element of the carrier of T

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

the carrier of T is non empty set

X is Element of the carrier of T

waybelow X is non empty directed lower (T) Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

[#] T is non empty non proper directed lower upper Element of K32( the carrier of T)

(waybelow X) /\ ([#] T) is Element of K32( the carrier of T)

"\/" (((waybelow X) /\ ([#] T)),T) is Element of the carrier of T

X is Element of the carrier of T

A is Element of the carrier of T

{X,A} is finite Element of K32( the carrier of T)

"\/" ({X,A},T) is Element of the carrier of T

X is (T)

Top T is Element of the carrier of T

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

T is non empty antisymmetric lower-bounded RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict antisymmetric full SubRelStr of T

Bottom T is Element of the carrier of T

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

the carrier of (subrelstr X) is non empty set

A is Element of the carrier of (subrelstr X)

b is Element of the carrier of (subrelstr X)

c

T is non empty antisymmetric lower-bounded RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty (T) Element of K32( the carrier of T)

subrelstr X is non empty strict antisymmetric full SubRelStr of T

T is non empty reflexive transitive antisymmetric upper-bounded with_suprema up-complete satisfying_axiom_of_approximation continuous RelStr

X is (T)

the non empty set is non empty set

BoolePoset the non empty set is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded satisfying_axiom_K algebraic with_suprema with_infima complete up-complete /\-complete Boolean satisfying_axiom_of_approximation continuous RelStr

T is non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

X is directed (T) (T)

Top T is Element of the carrier of T

the carrier of T is non empty non trivial set

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

waybelow (Top T) is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

(waybelow (Top T)) /\ X is Element of K32( the carrier of T)

"\/" (((waybelow (Top T)) /\ X),T) is Element of the carrier of T

Bottom T is Element of the carrier of T

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

T is non empty reflexive transitive antisymmetric with_suprema RelStr

CompactSublatt T is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of T

the carrier of (CompactSublatt T) is set

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict reflexive transitive antisymmetric full SubRelStr of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded satisfying_axiom_K algebraic with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

CompactSublatt T is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of T

the carrier of (CompactSublatt T) is non empty set

the carrier of T is non empty set

K32( the carrier of T) is non empty set

A is Element of the carrier of T

compactbelow A is non empty directed Element of K32( the carrier of T)

"\/" ((compactbelow A),T) is Element of the carrier of T

waybelow A is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

X is directed (T) Element of K32( the carrier of T)

(waybelow A) /\ X is Element of K32( the carrier of T)

"\/" (((waybelow A) /\ X),T) is Element of the carrier of T

Bottom T is Element of the carrier of T

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

A is directed (T) (T)

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

CompactSublatt T is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of T

the carrier of (CompactSublatt T) is non empty set

the carrier of T is non empty set

K32( the carrier of T) is non empty set

A is Element of the carrier of T

waybelow A is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

X is Element of K32( the carrier of T)

(waybelow A) /\ X is Element of K32( the carrier of T)

"\/" (((waybelow A) /\ X),T) is Element of the carrier of T

compactbelow A is non empty directed Element of K32( the carrier of T)

"\/" ((compactbelow A),T) is Element of the carrier of T

A is Element of the carrier of T

compactbelow A is non empty directed Element of K32( the carrier of T)

b is Element of the carrier of T

compactbelow b is non empty directed Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is directed (T) Element of K32( the carrier of T)

b is Element of the carrier of T

A is Element of the carrier of T

waybelow b is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow b) /\ X is Element of K32( the carrier of T)

downarrow A is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

c

y is Element of the carrier of T

"\/" (((waybelow b) /\ X),T) is Element of the carrier of T

"\/" ((downarrow A),T) is Element of the carrier of T

A is Element of the carrier of T

waybelow A is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow A) /\ X is Element of K32( the carrier of T)

"\/" (((waybelow A) /\ X),T) is Element of the carrier of T

"\/" ((waybelow A),T) is Element of the carrier of T

b is Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( 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

X is directed (T) Element of K32( the carrier of T)

A is Element of the carrier of T

b is Element of the carrier of T

waybelow b is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow b) /\ X is Element of K32( the carrier of T)

c

"\/" (c

y is Element of the carrier of T

A is Element of the carrier of T

waybelow A is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow A) /\ X is Element of K32( the carrier of T)

"\/" (((waybelow A) /\ X),T) is Element of the carrier of T

b is Element of the carrier of T

waybelow b is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

c

waybelow c

b is Element of the carrier of T

c

"\/" ((waybelow A),T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( 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

CompactSublatt T is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of T

the carrier of (CompactSublatt T) is non empty set

X is directed (T) Element of K32( the carrier of T)

A is set

b is Element of the carrier of T

c

b is Element of the carrier of T

A is Element of the carrier of T

c

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

b is Element of the carrier of T

A is Element of the carrier of T

c

waybelow c

y is Element of the carrier of T

waybelow y is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

c

y is Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( 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

CompactSublatt T is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of T

the carrier of (CompactSublatt T) is non empty set

X is directed (T) Element of K32( the carrier of T)

A is Element of the carrier of T

b is Element of the carrier of T

b is Element of the carrier of T

A is Element of the carrier of T

b is Element of the carrier of T

A is Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

K32( 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

X is directed (T) Element of K32( the carrier of T)

A is Element of the carrier of T

b is Element of the carrier of T

b is Element of the carrier of T

A is Element of the carrier of T

b is Element of the carrier of T

A is Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded with_suprema 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

K32( the carrier of T) is non empty set

X is non empty reflexive transitive antisymmetric full SubRelStr of T

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is Element of the carrier of T

waybelow A is non empty directed lower (T) Element of K32( the carrier of T)

(waybelow A) /\ the carrier of X is Element of K32( the carrier of T)

y is Element of the carrier of X

y1 is Element of the carrier of X

b is non empty Element of K32( the carrier of X)

C is Element of the carrier of T

a is Element of the carrier of T

c

(waybelow A) /\ c

T is non empty reflexive transitive RelStr

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

the carrier of T is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of T) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T)) is non empty set

the carrier of X is non empty set

K32( the carrier of X) is non empty set

b is set

"\/" (b,T) is Element of the carrier of T

b is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

b is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

c

y is non empty directed lower Element of K32( the carrier of X)

c

"\/" (y,T) is Element of the carrier of T

{ b

RelIncl (Ids X) is V7() V10( Ids X) V11( Ids X) V17( Ids X) V166() V169() V173() Element of K32(K33((Ids X),(Ids X)))

K33((Ids X),(Ids X)) is non empty set

K32(K33((Ids X),(Ids X))) is non empty set

RelStr(# (Ids X),(RelIncl (Ids X)) #) is strict RelStr

the carrier of RelStr(# (Ids X),(RelIncl (Ids X)) #) is set

y is non empty directed lower Element of K32( the carrier of X)

c

"\/" (y,T) is Element of the carrier of T

b is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

c

RelIncl (Ids X) is V7() V10( Ids X) V11( Ids X) V17( Ids X) V166() V169() V173() Element of K32(K33((Ids X),(Ids X)))

K33((Ids X),(Ids X)) is non empty set

K32(K33((Ids X),(Ids X))) is non empty set

RelStr(# (Ids X),(RelIncl (Ids X)) #) is strict RelStr

the carrier of RelStr(# (Ids X),(RelIncl (Ids X)) #) is set

y is set

{ b

C is non empty directed lower Element of K32( the carrier of X)

y1 is non empty directed lower Element of K32( the carrier of X)

b . y1 is set

"\/" (y1,T) is Element of the carrier of T

b . y is set

c

dom c

K32( the carrier of (InclPoset (Ids X))) is non empty set

dom b is Element of K32( the carrier of (InclPoset (Ids X)))

T is non empty reflexive transitive RelStr

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T)))) is non empty set

the carrier of X is non empty set

K32( the carrier of X) is non empty set

the carrier of T is non empty set

K32( the carrier of T) is non empty set

c

{ b

y is non empty directed lower Element of K32( the carrier of X)

y1 is non empty directed Element of K32( the carrier of T)

downarrow y1 is non empty directed lower Element of K32( the carrier of T)

{ b

C is Element of the carrier of (InclPoset (Ids T))

c

c

y is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

y1 is non empty directed lower Element of K32( the carrier of X)

y . y1 is set

{ b

RelIncl (Ids X) is V7() V10( Ids X) V11( Ids X) V17( Ids X) V166() V169() V173() Element of K32(K33((Ids X),(Ids X)))

K33((Ids X),(Ids X)) is non empty set

K32(K33((Ids X),(Ids X))) is non empty set

RelStr(# (Ids X),(RelIncl (Ids X)) #) is strict RelStr

the carrier of RelStr(# (Ids X),(RelIncl (Ids X)) #) is set

C is Element of K32( the carrier of T)

downarrow C is lower Element of K32( the carrier of T)

a is Element of K32( the carrier of T)

downarrow a is lower Element of K32( the carrier of T)

y1 is non empty directed lower Element of K32( the carrier of X)

y . y1 is set

b is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

c

RelIncl (Ids X) is V7() V10( Ids X) V11( Ids X) V17( Ids X) V166() V169() V173() Element of K32(K33((Ids X),(Ids X)))

K33((Ids X),(Ids X)) is non empty set

K32(K33((Ids X),(Ids X))) is non empty set

RelStr(# (Ids X),(RelIncl (Ids X)) #) is strict RelStr

the carrier of RelStr(# (Ids X),(RelIncl (Ids X)) #) is set

y is set

{ b

C is non empty directed lower Element of K32( the carrier of X)

y1 is non empty directed lower Element of K32( the carrier of X)

c

b . y1 is set

b . y is set

c

C is Element of K32( the carrier of T)

downarrow C is lower Element of K32( the carrier of T)

a is Element of K32( the carrier of T)

downarrow a is lower Element of K32( the carrier of T)

dom c

K32( the carrier of (InclPoset (Ids X))) is non empty set

dom b is Element of K32( the carrier of (InclPoset (Ids X)))

T is reflexive RelStr

the carrier of T is set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict reflexive full SubRelStr of T

T is transitive RelStr

the carrier of T is set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict transitive full SubRelStr of T

T is antisymmetric RelStr

the carrier of T is set

K32( the carrier of T) is non empty set

X is Element of K32( the carrier of T)

subrelstr X is strict antisymmetric full SubRelStr of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

X is non empty directed (T) (T) (T)

subrelstr X is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of T

Ids (subrelstr X) is non empty set

InclPoset (Ids (subrelstr X)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

the carrier of (InclPoset (Ids (subrelstr X))) is non empty set

K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X))))) is non empty set

b is Element of the carrier of T

the carrier of (subrelstr X) is non empty set

Bottom T is Element of the carrier of T

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

c

waybelow c

K32( the carrier of T) is non empty set

(waybelow c

K32( the carrier of (subrelstr X)) is non empty set

y is Element of the carrier of (InclPoset (Ids (subrelstr X)))

b is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

b is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

c

y is Element of the carrier of T

c

waybelow y is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

(waybelow y) /\ X is Element of K32( the carrier of T)

y1 is Element of the carrier of T

waybelow y1 is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow y1) /\ X is Element of K32( the carrier of T)

y is Element of the carrier of T

c

waybelow y is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow y) /\ X is Element of K32( the carrier of T)

A is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

b is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

c

A . c

y is Element of the carrier of T

waybelow y is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

(waybelow y) /\ X is Element of K32( the carrier of T)

b . c

dom b is Element of K32( the carrier of T)

dom A is Element of K32( the carrier of T)

T is non empty reflexive transitive RelStr

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

K33( the carrier of (InclPoset (Ids X)), the carrier of T) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T)) is non empty set

dom (T,X) is Element of K32( the carrier of (InclPoset (Ids X)))

K32( the carrier of (InclPoset (Ids X))) is non empty set

rng (T,X) is Element of K32( the carrier of T)

RelIncl (Ids X) is V7() V10( Ids X) V11( Ids X) V17( Ids X) V166() V169() V173() Element of K32(K33((Ids X),(Ids X)))

K33((Ids X),(Ids X)) is non empty set

K32(K33((Ids X),(Ids X))) is non empty set

RelStr(# (Ids X),(RelIncl (Ids X)) #) is strict RelStr

the carrier of RelStr(# (Ids X),(RelIncl (Ids X)) #) is set

T is non empty reflexive transitive RelStr

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

the carrier of T is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of T) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T)) is non empty set

dom (T,X) is Element of K32( the carrier of (InclPoset (Ids X)))

K32( the carrier of (InclPoset (Ids X))) is non empty set

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is set

{ b

b is non empty directed lower Element of K32( the carrier of X)

T is non empty reflexive transitive RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

K32((Ids T)) is non empty set

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T)))) is non empty set

dom (T,X) is Element of K32( the carrier of (InclPoset (Ids X)))

K32( the carrier of (InclPoset (Ids X))) is non empty set

rng (T,X) is Element of K32( the carrier of (InclPoset (Ids T)))

K32( the carrier of (InclPoset (Ids T))) is non empty set

RelIncl (Ids X) is V7() V10( Ids X) V11( Ids X) V17( Ids X) V166() V169() V173() Element of K32(K33((Ids X),(Ids X)))

K33((Ids X),(Ids X)) is non empty set

K32(K33((Ids X),(Ids X))) is non empty set

RelStr(# (Ids X),(RelIncl (Ids X)) #) is strict RelStr

the carrier of RelStr(# (Ids X),(RelIncl (Ids X)) #) is set

T is non empty reflexive transitive RelStr

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T)))) is non empty set

dom (T,X) is Element of K32( the carrier of (InclPoset (Ids X)))

K32( the carrier of (InclPoset (Ids X))) is non empty set

the carrier of X is non empty set

K32( the carrier of X) is non empty set

A is set

{ b

b is non empty directed lower Element of K32( the carrier of X)

T is non empty reflexive transitive RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

the carrier of T is non empty set

K32( the carrier of T) is non empty set

X is non empty reflexive transitive full SubRelStr of T

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids X)) is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T)))) is non empty set

rng (T,X) is Element of K32( the carrier of (InclPoset (Ids T)))

K32( the carrier of (InclPoset (Ids T))) is non empty set

A is set

K32((Ids T)) is non empty set

{ b

b is non empty directed lower Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

A is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

X is non empty directed (T) (T) (T)

(T,X) is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

subrelstr X is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of T

Ids (subrelstr X) is non empty set

InclPoset (Ids (subrelstr X)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

the carrier of (InclPoset (Ids (subrelstr X))) is non empty set

K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X))))) is non empty set

dom (T,X) is Element of K32( the carrier of T)

K32( the carrier of T) is non empty set

b is non empty directed (A) (A) (A)

subrelstr b is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of A

Ids (subrelstr b) is non empty set

InclPoset (Ids (subrelstr b)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

the carrier of (InclPoset (Ids (subrelstr b))) is non empty set

(A,b) is V7() V10( the carrier of A) V11( the carrier of (InclPoset (Ids (subrelstr b)))) Function-like quasi_total Element of K32(K33( the carrier of A, the carrier of (InclPoset (Ids (subrelstr b)))))

the carrier of A is non empty set

K33( the carrier of A, the carrier of (InclPoset (Ids (subrelstr b)))) is non empty set

K32(K33( the carrier of A, the carrier of (InclPoset (Ids (subrelstr b))))) is non empty set

rng (A,b) is Element of K32( the carrier of (InclPoset (Ids (subrelstr b))))

K32( the carrier of (InclPoset (Ids (subrelstr b)))) is non empty set

K32((Ids (subrelstr b))) is non empty set

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

X is non empty directed (T) (T) (T)

subrelstr X is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of T

Ids (subrelstr X) is non empty set

InclPoset (Ids (subrelstr X)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

the carrier of (InclPoset (Ids (subrelstr X))) is non empty set

(T,X) is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

the carrier of T is non empty set

K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X))))) is non empty set

rng (T,X) is Element of K32( the carrier of (InclPoset (Ids (subrelstr X))))

K32( the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

the carrier of (subrelstr X) is non empty set

K32( the carrier of (subrelstr X)) is non empty set

A is set

K32((Ids (subrelstr X))) is non empty set

{ b

b is non empty directed lower Element of K32( the carrier of (subrelstr X))

T is non empty reflexive transitive antisymmetric up-complete RelStr

X is non empty reflexive transitive antisymmetric full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

the carrier of (InclPoset (Ids X)) is non empty set

the carrier of T is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of T) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T)) is non empty set

the carrier of X is non empty set

K32( the carrier of X) is non empty set

b is Element of the carrier of (InclPoset (Ids X))

c

y is non empty directed lower Element of K32( the carrier of X)

y1 is non empty directed lower Element of K32( the carrier of X)

K32( the carrier of T) is non empty set

(T,X) . c

"\/" (y1,T) is Element of the carrier of T

(T,X) . b is Element of the carrier of T

"\/" (y,T) is Element of the carrier of T

T is non empty reflexive transitive RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

the carrier of (InclPoset (Ids X)) is non empty set

the carrier of (InclPoset (Ids T)) is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T)))) is non empty set

the carrier of X is non empty set

K32( the carrier of X) is non empty set

b is Element of the carrier of (InclPoset (Ids X))

c

the carrier of T is non empty set

K32( the carrier of T) is non empty set

y is non empty directed lower Element of K32( the carrier of X)

(T,X) . b is Element of the carrier of (InclPoset (Ids T))

C is Element of K32( the carrier of T)

downarrow C is lower Element of K32( the carrier of T)

y1 is non empty directed lower Element of K32( the carrier of X)

(T,X) . c

a is Element of K32( the carrier of T)

downarrow a is lower Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

X is non empty directed (T) (T) (T)

subrelstr X is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of T

Ids (subrelstr X) is non empty set

InclPoset (Ids (subrelstr X)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

(T,X) is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

the carrier of T is non empty set

the carrier of (InclPoset (Ids (subrelstr X))) is non empty set

K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X))))) is non empty set

b is Element of the carrier of T

c

(T,X) . c

waybelow c

K32( the carrier of T) is non empty set

(waybelow c

(T,X) . b is Element of the carrier of (InclPoset (Ids (subrelstr X)))

waybelow b is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)

(waybelow b) /\ X is Element of K32( the carrier of T)

T is non empty reflexive transitive antisymmetric up-complete RelStr

X is non empty reflexive transitive antisymmetric full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))

the carrier of (InclPoset (Ids X)) is non empty set

the carrier of T is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of T) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T)) is non empty set

T is non empty reflexive transitive RelStr

X is non empty reflexive transitive full SubRelStr of T

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))))

the carrier of (InclPoset (Ids X)) is non empty set

the carrier of (InclPoset (Ids T)) is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of (InclPoset (Ids T)))) is non empty set

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

X is non empty directed (T) (T) (T)

subrelstr X is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of T

Ids (subrelstr X) is non empty set

InclPoset (Ids (subrelstr X)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

(T,X) is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))

the carrier of T is non empty set

the carrier of (InclPoset (Ids (subrelstr X))) is non empty set

K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X))))) is non empty set

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

Ids T is non empty set

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

X is non empty directed (T) (T) (T)

subrelstr X is non empty strict reflexive transitive antisymmetric lower-bounded full with_suprema SubRelStr of T

Ids (subrelstr X) is non empty set

InclPoset (Ids (subrelstr X)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima complete up-complete /\-complete RelStr

(T,(subrelstr X)) is V7() V10( the carrier of (InclPoset (Ids (subrelstr X)))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of (InclPoset (Ids T))))

the carrier of (InclPoset (Ids (subrelstr X))) is non empty set

the carrier of (InclPoset (Ids T)) is non empty set

K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of (InclPoset (Ids T))) is non empty set

K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of (InclPoset (Ids T)))) is non empty set

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

the carrier of (subrelstr X) is non empty set

K32( the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set

K32( the carrier of (subrelstr X)) is non empty set

b is Element of K32( the carrier of (InclPoset (Ids (subrelstr X))))

"\/" (b,(InclPoset (Ids (subrelstr X)))) is Element of the carrier of (InclPoset (Ids (subrelstr X)))

K32( the carrier of T) is non empty set

((subrelstr X),b) is Element of K32( the carrier of (subrelstr X))

finsups ((subrelstr X),b) is non empty directed Element of K32( the carrier of (subrelstr X))

downarrow (finsups ((subrelstr X),b)) is non empty directed lower Element of K32( the carrier of (subrelstr X))

c

(T,(subrelstr X)) . c

(T,(subrelstr X)) .: b is Element of K32( the carrier of (InclPoset (Ids T)))

K32( the carrier of (InclPoset (Ids T))) is non empty set

(T,((T,(subrelstr X)) .: b)) is Element of K32( the carrier of T)

finsups (T,((T,(subrelstr X)) .: b)) is non empty directed Element of K32( the carrier of T)

downarrow (finsups (T,((T,(subrelstr X)) .: b))) is non empty directed lower Element of K32( the carrier of T)

y1 is Element of K32( the carrier of T)

downarrow y1 is lower Element of K32( the carrier of T)

a is set

a1 is Element of the carrier of T

a2 is Element of the carrier of T

K32((T,((T,(subrelstr X)) .: b))) is non empty set

{ ("\/" (b

d1 is finite Element of K32((T,((T,(subrelstr X)) .: b)))

"\/" (d1,T) is Element of the carrier of T

d2 is set

Z is set

dom (T,(subrelstr X)) is Element of K32( the carrier of (InclPoset (Ids (subrelstr X))))

xl is set

(T,(subrelstr X)) . xl is set

srg is Element of the carrier of (InclPoset (Ids (subrelstr X)))

(T,(subrelstr X)) . srg is Element of the carrier of (InclPoset (Ids T))

b is Element of the carrier of (InclPoset (Ids T))

c1 is non empty directed lower Element of K32( the carrier of (subrelstr X))

(T,(subrelstr X)) . c1 is set

c is Element of K32( the carrier of T)

downarrow c is lower Element of K32( the carrier of T)

b1 is Element of the carrier of T

z2 is Element of the carrier of T

v is Element of X

K33(d1,X) is set

K32(K33(d1,X)) is non empty set

d2 is V7() V10(d1) V11(X) Function-like