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
c5 is non empty directed lower Element of K32( the carrier of T)
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
{ ("\/" (b1,T)) where b1 is finite Element of K32(X) : ex_sup_of b1,T } is set
c5 is finite Element of K32(X)
"\/" (c5,T) is Element of the carrier of T
K32(A) is non empty set
y is finite Element of K32(A)
{ ("\/" (b1,T)) where b1 is finite Element of K32(A) : ex_sup_of b1,T } is 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 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)
c5 is set
K32(A) is non empty set
{ ("\/" (b1,T)) where b1 is finite Element of K32(A) : ex_sup_of b1,T } is set
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
{ ("\/" (b1,X)) where b1 is finite Element of K32(b) : ex_sup_of b1,X } is set
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)
c5 is set
K32(b) is non empty set
{ ("\/" (b1,X)) where b1 is finite Element of K32(b) : ex_sup_of b1,X } is set
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
{ ("\/" (b1,T)) where b1 is finite Element of K32(A) : ex_sup_of b1,T } is set
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)
c5 is set
K32(b) is non empty set
{ ("\/" (b1,X)) where b1 is finite Element of K32(b) : ex_sup_of b1,X } is set
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
{ ("\/" (b1,T)) where b1 is finite Element of K32(A) : ex_sup_of b1,T } is set
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
{ ("\/" (b1,T)) where b1 is finite Element of K32(A) : ex_sup_of b1,T } is set
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))
c5 is non empty directed lower Element of K32( the carrier of T)
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
c5 is Element of the carrier of T
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
c5 is Element of the carrier of T
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
c5 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
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
c5 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)
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)
c5 is set
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)
c5 is set
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
c5 is Element of the carrier of T
{b,c5} is finite Element of K32( the carrier of T)
the carrier of (subrelstr A) is set
"\/" ({b,c5},T) is Element of the carrier of T
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
c5 is Element of the carrier of T
{b,c5} is finite Element of K32( the carrier of T)
the carrier of (subrelstr A) is set
"/\" ({b,c5},T) is Element of the carrier of T
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
c5 is Element of the carrier of T
{b,c5} is finite Element of K32( the carrier of T)
A is Element of the carrier of T
b "\/" c5 is Element of the carrier of T
"\/" ({b,c5},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
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
c5 is Element of the carrier of T
{b,c5} is finite Element of K32( the carrier of T)
A is Element of the carrier of T
b "/\" c5 is Element of the carrier of T
"/\" ({b,c5},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
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
c5 is Element of the carrier of T
{b,c5} is finite Element of K32( the carrier of T)
A is Element of the carrier of T
b "\/" c5 is Element of the carrier of T
"\/" ({b,c5},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
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
c5 is Element of the carrier of T
{b,c5} is finite Element of K32( the carrier of T)
A is Element of the carrier of T
A "/\" A is Element of the carrier of T
b "/\" c5 is Element of the carrier of T
"/\" ({b,c5},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
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 b1) where b1 is V63(T) V231(T) Element of K32(K32( the carrier of T)) : verum } is set
meet { (card b1) where b1 is V63(T) V231(T) Element of K32(K32( the carrier of T)) : verum } is set
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
c5 is V63(T) V231(T) Element of K32(K32( the carrier of T))
card c5 is ordinal cardinal set
c5 is set
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)
c5 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
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)
c5 is set
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)
c5 is non empty directed Element of K32( the carrier of T)
"\/" (c5,T) is Element of the carrier of T
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)
c5 is Element of the carrier of T
waybelow c5 is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
b is Element of the carrier of T
c5 is Element of the carrier of T
"\/" ((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
c5 is Element of the carrier of T
b is Element of the carrier of T
A is Element of the carrier of T
c5 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
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
c5 is Element of the carrier of T
waybelow c5 is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
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)
c5 is Element of the carrier of T
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
c5 is directed (T) Element of K32( the carrier of T)
(waybelow A) /\ c5 is Element of K32( the carrier of T)
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))
c5 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))
y is non empty directed lower Element of K32( the carrier of X)
c5 . y is set
"\/" (y,T) is Element of the carrier of T
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is 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
y is non empty directed lower Element of K32( the carrier of X)
c5 . y is set
"\/" (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))
c5 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))
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is set
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
c5 . y is set
dom c5 is Element of K32( the carrier of (InclPoset (Ids X)))
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
c5 is Element of the carrier of (InclPoset (Ids X))
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is set
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)
{ b1 where b1 is non empty directed lower Element of K32( the carrier of T) : verum } is set
C is Element of the carrier of (InclPoset (Ids T))
c5 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))))
c5 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))))
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is 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
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))))
c5 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))))
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is set
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)
c5 . y1 is set
b . y1 is set
b . y is set
c5 . y 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)
dom c5 is Element of K32( the carrier of (InclPoset (Ids X)))
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
c5 is Element of the carrier of T
waybelow c5 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 c5) /\ X is Element of K32( the carrier of T)
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)))))
c5 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)))))
y is Element of the carrier of T
c5 . y is Element of the carrier of (InclPoset (Ids (subrelstr X)))
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
c5 . y is Element of the carrier of (InclPoset (Ids (subrelstr X)))
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)))))
c5 is set
A . c5 is set
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 . c5 is set
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is set
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of X) : verum } is set
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of T) : verum } is set
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of (subrelstr X)) : verum } is set
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))
c5 is Element of the carrier of (InclPoset (Ids X))
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) . c5 is Element of the carrier of T
"\/" (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))
c5 is Element of the carrier of (InclPoset (Ids X))
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) . c5 is Element of the carrier of (InclPoset (Ids T))
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
c5 is Element of the carrier of T
(T,X) . c5 is Element of the carrier of (InclPoset (Ids (subrelstr X)))
waybelow c5 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 c5) /\ X is Element of K32( the carrier of T)
(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))
c5 is non empty directed lower Element of K32( the carrier of (subrelstr X))
(T,(subrelstr X)) . c5 is set
(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
{ ("\/" (b1,T)) where b1 is finite Element of K32((T,((T,(subrelstr X)) .: b))) : ex_sup_of b1,T } is set
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 quasi_total finite Element of K32(K33(d1,X))
rng d2 is finite Element of K32(X)
K32(X) is non empty set
dom d2 is finite Element of K32(d1)
K32(d1) is non empty finite V32() set
"\/" ((rng d2),T) is Element of the carrier of T
xl is Element of the carrier of T
d2 . xl is set
b is Element of the carrier of T
b1 is Element of the carrier of T
srg is Element of the carrier of (InclPoset (Ids (subrelstr X)))
Z is finite Element of K32( the carrier of (subrelstr X))
xl is set
srg is set
d2 . srg is set
b1 is Element of the carrier of T
c1 is Element of the carrier of T
b is Element of the carrier of (InclPoset (Ids (subrelstr X)))
"\/" (Z,(subrelstr X)) is Element of the carrier of (subrelstr X)
K32(((subrelstr X),b)) is non empty set
{ ("\/" (b1,(subrelstr X))) where b1 is finite Element of K32(((subrelstr X),b)) : ex_sup_of b1, subrelstr X } is set
"\/" ((rng d2),(subrelstr X)) is Element of the carrier of (subrelstr X)
"\/" (Z,T) is Element of the carrier of T
b is Element of the carrier of (subrelstr X)
b1 is Element of the carrier of T
c1 is Element of the carrier of T
c is Element of the carrier of (subrelstr X)
xl is Element of the carrier of (subrelstr X)
b is Element of the carrier of (subrelstr X)
b1 is Element of the carrier of T
srg is Element of the carrier of T
a is set
a1 is non empty directed lower Element of K32( the carrier of (subrelstr X))
(T,(subrelstr X)) . a1 is set
a2 is Element of K32( the carrier of T)
downarrow a2 is lower Element of K32( the carrier of T)
dom (T,(subrelstr X)) is Element of K32( the carrier of (InclPoset (Ids (subrelstr X))))
d1 is set
y is Element of K32( the carrier of T)
finsups y is non empty directed Element of K32( the carrier of T)
C is Element of K32( the carrier of T)
downarrow C is lower Element of K32( the carrier of T)
downarrow (downarrow (finsups (T,((T,(subrelstr X)) .: b)))) is non empty directed lower Element of K32( the carrier of T)
"\/" (((T,(subrelstr X)) .: b),(InclPoset (Ids T))) is Element of the carrier of (InclPoset (Ids T))
(T,(subrelstr X)) . ("\/" (b,(InclPoset (Ids (subrelstr X))))) is Element of the carrier of (InclPoset (Ids T))
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 up-complete RelStr
the carrier of T 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
SupMap T is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids T)), the carrier of T))
K33( the carrier of (InclPoset (Ids T)), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids T)), the carrier of T)) is non empty set
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
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 monotone 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
(T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total monotone 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
(SupMap T) * (T,X) is V7() V10( the carrier of (InclPoset (Ids X))) V11( the carrier of T) Function-like Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of T))
A is 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
dom (T,X) is Element of K32( the carrier of (InclPoset (Ids X)))
(T,X) . A is set
dom (SupMap T) is Element of K32( the carrier of (InclPoset (Ids T)))
K32( 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
rng (T,X) is Element of K32( the carrier of (InclPoset (Ids T)))
K32( 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
A is set
the carrier of X is non empty set
K32( the carrier of X) is non empty set
K32( the carrier of T) is non empty set
b is non empty directed lower Element of K32( the carrier of X)
(T,X) . b is set
c5 is Element of K32( the carrier of T)
downarrow c5 is lower Element of K32( the carrier of T)
y is non empty directed Element of K32( the carrier of T)
(T,X) . A is set
"\/" (b,T) is Element of the carrier of T
downarrow y is non empty directed lower Element of K32( the carrier of T)
"\/" ((downarrow y),T) is Element of the carrier of T
(T,X) . A is set
(SupMap T) . ((T,X) . A) is 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,(subrelstr X)) is V7() V10( the carrier of (InclPoset (Ids (subrelstr X)))) V11( the carrier of T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T))
the carrier of (InclPoset (Ids (subrelstr X))) is non empty set
the carrier of T is non empty set
K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T)) 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 monotone Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))
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,(subrelstr X)),(T,X)] is Connection of InclPoset (Ids (subrelstr X)),T
{(T,(subrelstr X)),(T,X)} is finite set
{(T,(subrelstr X))} is non empty trivial finite 1 -element set
{{(T,(subrelstr X)),(T,X)},{(T,(subrelstr X))}} is finite V32() set
the carrier of (subrelstr X) is non empty set
K32( the carrier of (subrelstr X)) is non empty set
b is Element of the carrier of (InclPoset (Ids (subrelstr X)))
K32( the carrier of T) is non empty set
c5 is non empty directed lower Element of K32( the carrier of (subrelstr X))
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)
(T,(subrelstr X)) . b is Element of the carrier of T
(T,X) . A is Element of the carrier of (InclPoset (Ids (subrelstr X)))
y is non empty directed Element of K32( the carrier of T)
downarrow y is non empty directed lower Element of K32( the carrier of T)
(downarrow y) /\ X is Element of K32( the carrier of T)
y1 is set
C is Element of the carrier of T
a1 is Element of the carrier of T
a is Element of the carrier of (subrelstr X)
a2 is Element of the carrier of (subrelstr X)
"\/" (c5,T) is Element of the carrier of T
"\/" ((downarrow y),T) is Element of the carrier of T
y1 is set
C is Element of the carrier of T
y is non empty directed Element of K32( the carrier of T)
"\/" (((waybelow A) /\ X),T) is Element of the carrier of T
"\/" (y,T) is Element of the carrier of T
"\/" (c5,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
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 T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T))
the carrier of (InclPoset (Ids (subrelstr X))) is non empty set
the carrier of T is non empty set
K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T)) 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 monotone Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))
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,(subrelstr X)),(T,X)] is Connection of InclPoset (Ids (subrelstr X)),T
{(T,(subrelstr X)),(T,X)} is finite set
{(T,(subrelstr X))} is non empty trivial finite 1 -element set
{{(T,(subrelstr X)),(T,X)},{(T,(subrelstr X))}} is finite V32() 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
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
(T,(subrelstr X)) is V7() V10( the carrier of (InclPoset (Ids (subrelstr X)))) V11( the carrier of T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier 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 (InclPoset (Ids (subrelstr X))), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T)) is non empty set
rng (T,(subrelstr X)) is Element of K32( the carrier of T)
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
A is set
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)
K32(X) is non empty set
the carrier of (subrelstr X) is non empty set
K32( the carrier of (subrelstr X)) is non empty set
y1 is Element of the carrier of (subrelstr X)
C is Element of the carrier of (subrelstr X)
y is Element of K32( the carrier of (subrelstr X))
a is Element of the carrier of T
a1 is Element of the carrier of T
y1 is non empty directed lower Element of K32( the carrier of (subrelstr X))
{ b1 where b1 is non empty directed lower Element of K32( the carrier of (subrelstr X)) : verum } is set
dom (T,(subrelstr X)) is Element of K32( the carrier of (InclPoset (Ids (subrelstr X))))
K32( the carrier of (InclPoset (Ids (subrelstr X)))) is non empty set
"\/" (y1,T) is Element of the carrier of T
(T,(subrelstr X)) . y1 is 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,(subrelstr X)) is V7() V10( the carrier of (InclPoset (Ids (subrelstr X)))) V11( the carrier of T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T))
the carrier of (InclPoset (Ids (subrelstr X))) is non empty set
the carrier of T is non empty set
K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T)) is non empty set
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
SupMap T is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids T)), the carrier of T))
the carrier of (InclPoset (Ids T)) is non empty set
K33( the carrier of (InclPoset (Ids T)), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids T)), the carrier of T)) is non empty set
(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))))
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
(SupMap T) * (T,(subrelstr X)) is V7() V10( the carrier of (InclPoset (Ids (subrelstr X)))) V11( the carrier of T) Function-like Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), 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 monotone 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
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 T) Function-like quasi_total monotone Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T))
the carrier of (InclPoset (Ids (subrelstr X))) is non empty set
the carrier of T is non empty set
K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T)) 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 monotone Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))
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
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
CompactSublatt (InclPoset (Ids (subrelstr X))) is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of InclPoset (Ids (subrelstr X))
the carrier of (CompactSublatt (InclPoset (Ids (subrelstr X)))) is non empty set
the carrier of (subrelstr X) is non empty set
{ (downarrow b1) where b1 is Element of the carrier of (subrelstr X) : verum } is set
A is set
the carrier of (InclPoset (Ids (subrelstr X))) is non empty set
b is Element of the carrier of (InclPoset (Ids (subrelstr X)))
c5 is Element of the carrier of (subrelstr X)
downarrow c5 is non empty directed lower ( subrelstr X) Element of K32( the carrier of (subrelstr X))
K32( the carrier of (subrelstr X)) is non empty set
A is set
the carrier of (InclPoset (Ids (subrelstr X))) is non empty set
c5 is Element of the carrier of (subrelstr X)
downarrow c5 is non empty directed lower ( subrelstr X) Element of K32( the carrier of (subrelstr X))
K32( the carrier of (subrelstr X)) is non empty set
b is Element of the carrier of (InclPoset (Ids (subrelstr X)))
c5 is Element of the carrier of (subrelstr X)
downarrow c5 is non empty directed lower ( subrelstr X) Element of K32( the carrier of (subrelstr X))
K32( the carrier of (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
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
CompactSublatt (InclPoset (Ids (subrelstr X))) is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of InclPoset (Ids (subrelstr X))
the carrier of (subrelstr X) is non empty set
K32( the carrier of (subrelstr X)) is non empty set
the carrier of (CompactSublatt (InclPoset (Ids (subrelstr X)))) is non empty set
A is Element of the carrier of (subrelstr X)
downarrow A is non empty directed lower ( subrelstr X) Element of K32( the carrier of (subrelstr X))
{ (downarrow b1) where b1 is Element of the carrier of (subrelstr X) : verum } is set
K33( the carrier of (subrelstr X), the carrier of (CompactSublatt (InclPoset (Ids (subrelstr X))))) is non empty set
K32(K33( the carrier of (subrelstr X), the carrier of (CompactSublatt (InclPoset (Ids (subrelstr X)))))) is non empty set
A is V7() V10( the carrier of (subrelstr X)) V11( the carrier of (CompactSublatt (InclPoset (Ids (subrelstr X))))) Function-like quasi_total Element of K32(K33( the carrier of (subrelstr X), the carrier of (CompactSublatt (InclPoset (Ids (subrelstr X))))))
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
X is non empty directed (T) (T) (T)
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 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
A is Element of the carrier of (InclPoset (Ids (subrelstr X)))
"\/" (A,T) is Element of the carrier of T
waybelow ("\/" (A,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 ("\/" (A,T))) /\ X is Element of K32( the carrier of T)
the carrier of (subrelstr X) is non empty set
K32( the carrier of (subrelstr X)) is non empty set
b is non empty directed lower Element of K32( the carrier of (subrelstr X))
c5 is non empty directed Element of K32( the carrier of T)
X \ c5 is Element of K32( the carrier of T)
(X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X) is Element of K32( the carrier of T)
C is Element of the carrier of T
a is Element of the carrier of T
waybelow C is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
(waybelow C) /\ ((X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X)) is Element of K32( the carrier of T)
a1 is Element of the carrier of T
(waybelow C) /\ X is Element of K32( the carrier of T)
a2 is Element of the carrier of T
a2 "\/" a is Element of the carrier of T
{a2,a} is finite Element of K32( the carrier of T)
"\/" ({a2,a},T) is Element of the carrier of T
X \ A is Element of K32( the carrier of T)
"\/" (((waybelow C) /\ X),T) is Element of the carrier of T
a1 is Element of the carrier of T
"\/" (((waybelow C) /\ ((X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X))),T) is Element of the carrier of T
C is Element of the carrier of T
waybelow C is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
(waybelow C) /\ X is Element of K32( the carrier of T)
(waybelow C) /\ ((X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X)) is Element of K32( the carrier of T)
a is set
a1 is Element of the carrier of T
"\/" (((waybelow C) /\ ((X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X))),T) is Element of the carrier of T
C is Element of the carrier of T
subrelstr ((X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X)) is strict reflexive transitive antisymmetric full SubRelStr of T
C is Element of the carrier of T
the carrier of (subrelstr ((X \ c5) \/ ((waybelow ("\/" (A,T))) /\ X))) is set
a is Element of the carrier of T
{C,a} is finite Element of K32( the carrier of T)
"\/" ({C,a},T) is Element of the carrier of T
a1 is Element of the carrier of (subrelstr X)
a2 is Element of the carrier of (subrelstr X)
a1 "\/" a2 is Element of the carrier of (subrelstr X)
X \ A is Element of K32( the carrier of T)
C "\/" a is Element of the carrier of T
X \ A is Element of K32( the carrier of T)
C "\/" a is Element of the carrier of T
X \ A is Element of K32( the carrier of T)
C "\/" a is Element of the carrier of T
C "\/" a is Element of the carrier of T
X \ A is Element of K32( the carrier of T)
Bottom T is Element of the carrier of T
"\/" ({},T) is Element of the carrier of T
C is directed (T) (T)
a is set
a is set
a1 is Element of the carrier of T
d1 is Element of the carrier of T
a2 is Element of the carrier of (subrelstr X)
d2 is Element of the carrier of (subrelstr X)
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
the carrier of T is non empty set
(T,(subrelstr X)) is V7() V10( the carrier of (InclPoset (Ids (subrelstr X)))) V10( the carrier of (InclPoset (Ids (subrelstr X)))) V11( the carrier of T) Function-like quasi_total quasi_total monotone monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T))
K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr X))), the carrier of T)) is non empty set
A is Element of the carrier of (InclPoset (Ids (subrelstr X)))
b is Element of the carrier of (InclPoset (Ids (subrelstr X)))
(T,(subrelstr X)) . A is Element of the carrier of T
(T,(subrelstr X)) . b is Element of the carrier of T
the carrier of (subrelstr X) is non empty set
K32( the carrier of (subrelstr X)) is non empty set
y is non empty directed lower Element of K32( the carrier of (subrelstr X))
(T,(subrelstr X)) . y is set
"\/" (y,T) is Element of the carrier of T
c5 is non empty directed lower Element of K32( the carrier of (subrelstr X))
(T,(subrelstr X)) . c5 is set
"\/" (c5,T) is Element of the carrier of T
waybelow ("\/" (c5,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 ("\/" (y,T)) is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
(waybelow ("\/" (c5,T))) /\ X is Element of K32( the carrier of T)
(waybelow ("\/" (y,T))) /\ X is Element of K32( the carrier of T)
"\/" (b,T) is Element of the carrier of T
waybelow ("\/" (b,T)) is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
(waybelow ("\/" (b,T))) /\ X is Element of K32( the carrier of T)
"\/" (A,T) is Element of the carrier of T
waybelow ("\/" (A,T)) is non empty directed filtered lower (T) (T) Element of K32( the carrier of T)
(waybelow ("\/" (A,T))) /\ X is Element of K32( the carrier of T)
(T,X) is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids (subrelstr X)))) Function-like quasi_total monotone sups-preserving join-preserving directed-sups-preserving Element of K32(K33( the carrier of T, the carrier of (InclPoset (Ids (subrelstr X)))))
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
A is set
"\/" (A,T) is Element of the carrier of T
waybelow ("\/" (A,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 ("\/" (A,T))) /\ X is Element of K32( the carrier of T)
(T,X) . ("\/" (A,T)) is Element of the carrier of (InclPoset (Ids (subrelstr X)))
dom (T,X) is Element of K32( the carrier of T)
[(T,(subrelstr X)),(T,X)] is Connection of InclPoset (Ids (subrelstr X)),T
{(T,(subrelstr X)),(T,X)} is finite set
{(T,(subrelstr X))} is non empty trivial finite 1 -element set
{{(T,(subrelstr X)),(T,X)},{(T,(subrelstr X))}} is finite V32() set
rng (T,(subrelstr X)) is Element of K32( the carrier of T)
K32( the carrier of 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
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 non empty directed (T) (T) (T)
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
CompactSublatt A is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of A
the carrier of (CompactSublatt A) 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
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 non empty directed (T) (T) (T)
X is non empty directed (T) (T) (T)
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
(T) is ordinal cardinal set
{ (card b1) where b1 is V63(T) V231(T) Element of K32(K32( the carrier of T)) : verum } is set
meet { (card b1) where b1 is V63(T) V231(T) Element of K32(K32( the carrier of T)) : verum } is set
X is V63(T) V231(T) Element of K32(K32( the carrier of T))
card X is ordinal cardinal 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
(T) is ordinal cardinal set
{ (card b1) where b1 is V63(T) V231(T) Element of K32(K32( the carrier of T)) : verum } is set
meet { (card b1) where b1 is V63(T) V231(T) Element of K32(K32( the carrier of T)) : verum } is set
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
b is V63(T) V231(T) Element of K32(K32( the carrier of T))
card b is ordinal cardinal set
c5 is 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