:: YELLOW_4 semantic presentation

K113() is set
K32(K113()) is set
{} is set
the empty set is empty set
1 is non empty set
L is RelStr
the carrier of L is set
D1 is set
"\/" (D1,L) is Element of the carrier of L
D2 is Element of the carrier of L
L is RelStr
the carrier of L is set
D1 is set
"/\" (D1,L) is Element of the carrier of L
D2 is Element of the carrier of L
L is RelStr
the carrier of L is set
K32( the carrier of L) is set
L is non empty reflexive RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
q is Element of K32( the carrier of L)
s is Element of the carrier of L
x is Element of the carrier of L
q is Element of K32( the carrier of L)
s is Element of the carrier of L
x is Element of the carrier of L
L is RelStr
the carrier of L is set
K32( the carrier of L) is set
{} L is empty directed filtered Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
L is transitive RelStr
the carrier of L is set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
s is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
L is RelStr
the carrier of L is set
K32( the carrier of L) is set
D2 is Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
q is set
s is Element of the carrier of L
x is Element of the carrier of L
L is RelStr
the carrier of L is set
K32( the carrier of L) is set
{} L is empty directed filtered Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
L is transitive RelStr
the carrier of L is set
K32( the carrier of L) is set
D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
s is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
L is RelStr
the carrier of L is set
K32( the carrier of L) is set
D2 is Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
q is set
s is Element of the carrier of L
x is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "\/" x is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
(L,s,q) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in s & b₂ in q ) } is set
x is set
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
x is set
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
{} L is empty directed filtered Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
(L,D1,({} L)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in {} L ) } is set
D2 is set
q is Element of the carrier of L
s is Element of the carrier of L
q "\/" s is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
q is Element of the carrier of L
D1 is Element of K32( the carrier of L)
s is Element of the carrier of L
D2 is Element of K32( the carrier of L)
q "\/" s is Element of the carrier of L
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
the Element of D2 is Element of D2
q "\/" the Element of D2 is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
s is Element of the carrier of L
x is Element of the carrier of L
s "\/" x is Element of the carrier of L
L is non empty reflexive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
(L,D1,D1) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D1 ) } is set
D2 is set
q is non empty Element of K32( the carrier of L)
s is Element of q
s "\/" s is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of K32( the carrier of L)
(L,(L,D1,D2),q) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in (L,D1,D2) & b₂ in q ) } is set
(L,D2,q) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D2 & b₂ in q ) } is set
(L,D1,(L,D2,q)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in (L,D2,q) ) } is set
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
b is Element of the carrier of L
B1 is Element of the carrier of L
b "\/" B1 is Element of the carrier of L
B1 "\/" a is Element of the carrier of L
b "\/" (B1 "\/" a) is Element of the carrier of L
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
b is Element of the carrier of L
B1 is Element of the carrier of L
b "\/" B1 is Element of the carrier of L
x "\/" b is Element of the carrier of L
(x "\/" b) "\/" B1 is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is non empty Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is set
x is set
a is Element of D1
s is Element of D2
a "\/" s is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is directed Element of K32( the carrier of L)
D2 is directed Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
s is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
B1 is Element of the carrier of L
b1 is Element of the carrier of L
B1 "\/" b1 is Element of the carrier of L
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "\/" A1 is Element of the carrier of L
z is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is filtered Element of K32( the carrier of L)
D2 is filtered Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
s is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
B1 is Element of the carrier of L
b1 is Element of the carrier of L
B1 "\/" b1 is Element of the carrier of L
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "\/" A1 is Element of the carrier of L
z is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is upper Element of K32( the carrier of L)
D2 is upper Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
s is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
B1 is Element of the carrier of L
B1 is Element of the carrier of L
x "\/" x is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
{ (D2 "\/" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "\/" x is Element of the carrier of L
q is set
s is Element of the carrier of L
D2 "\/" s is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D2 \/ q is Element of K32( the carrier of L)
(L,D1,(D2 \/ q)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 \/ q ) } is set
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
(L,D1,q) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in q ) } is set
(L,D1,D2) \/ (L,D1,q) is Element of K32( the carrier of L)
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
L is non empty reflexive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
(L,D2,q) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D2 & b₂ in q ) } is set
D1 \/ (L,D2,q) is Element of K32( the carrier of L)
D1 \/ D2 is Element of K32( the carrier of L)
D1 \/ q is Element of K32( the carrier of L)
(L,(D1 \/ D2),(D1 \/ q)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 \/ D2 & b₂ in D1 \/ q ) } is set
s is set
x is Element of the carrier of L
x "\/" x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is upper Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
D1 \/ D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D1 \/ q is Element of K32( the carrier of L)
(L,(D1 \/ D2),(D1 \/ q)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 \/ D2 & b₂ in D1 \/ q ) } is set
(L,D2,q) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D2 & b₂ in q ) } is set
D1 \/ (L,D2,q) is Element of K32( the carrier of L)
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2} ) } is set
D1 "\/" D2 is Element of the carrier of L
{(D1 "\/" D2)} is Element of K32( the carrier of L)
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "\/" x is Element of the carrier of L
q is set
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
q is Element of the carrier of L
{D2,q} is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2,q} ) } is set
D1 "\/" D2 is Element of the carrier of L
D1 "\/" q is Element of the carrier of L
{(D1 "\/" D2),(D1 "\/" q)} is Element of K32( the carrier of L)
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
s is set
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D1},{D2}) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2} ) } is set
D1 "\/" D2 is Element of the carrier of L
{(D1 "\/" D2)} is Element of K32( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
q is Element of the carrier of L
{D2,q} is Element of K32( the carrier of L)
(L,{D1},{D2,q}) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2,q} ) } is set
D1 "\/" D2 is Element of the carrier of L
D1 "\/" q is Element of the carrier of L
{(D1 "\/" D2),(D1 "\/" q)} is Element of K32( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
x is set
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
L is non empty reflexive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
{ (D2 "\/" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
q is set
s is Element of the carrier of L
D2 "\/" s is Element of the carrier of L
q is set
s is non empty Element of K32( the carrier of L)
x is Element of s
D2 "\/" x is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
q is Element of the carrier of L
{ (D2 "\/" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
s is Element of the carrier of L
D2 "\/" s is Element of the carrier of L
x is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
"/\" (D1,L) is Element of the carrier of L
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
D2 "\/" ("/\" (D1,L)) is Element of the carrier of L
"/\" ((L,{D2},D1),L) is Element of the carrier of L
{ (D2 "\/" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
q is Element of the carrier of L
s is Element of the carrier of L
D2 "\/" s is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
"\/" ((L,D1,D2),L) is Element of the carrier of L
the Element of D2 is Element of D2
s is Element of the carrier of L
s "\/" the Element of D2 is Element of the carrier of L
x is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of the carrier of L
D2 is Element of the carrier of L
D1 "\/" D2 is Element of the carrier of L
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of the carrier of L
D2 is Element of the carrier of L
D1 "\/" D2 is Element of the carrier of L
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() up-complete /\-complete RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is non empty Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is non empty Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
"\/" ((L,D1,D2),L) is Element of the carrier of L
"\/" (D1,L) is Element of the carrier of L
"\/" (D2,L) is Element of the carrier of L
("\/" (D1,L)) "\/" ("\/" (D2,L)) is Element of the carrier of L
("\/" ((L,D1,D2),L)) "\/" ("\/" ((L,D1,D2),L)) is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
downarrow (L,D1,D2) is Element of K32( the carrier of L)
q is set
x is set
a is non empty Element of K32( the carrier of L)
b is Element of a
s is Element of D2
b "\/" s is Element of the carrier of L
B1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,D1,D2) ) } is set
(L,a,D2) is non empty Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in a & b₂ in D2 ) } is set
L is non empty reflexive transitive antisymmetric with_suprema RelStr
Ids L is non empty set
the carrier of L is non empty set
K32( the carrier of L) is set
{ b₁ where b₁ is non empty directed lower Element of K32( the carrier of L) : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema RelStr
the carrier of (InclPoset (Ids L)) is non empty set
D1 is Element of the carrier of (InclPoset (Ids L))
D2 is Element of the carrier of (InclPoset (Ids L))
D1 "\/" D2 is Element of the carrier of (InclPoset (Ids L))
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
downarrow (L,q,s) is lower Element of K32( the carrier of L)
x is non empty directed Element of K32( the carrier of L)
a is non empty directed Element of K32( the carrier of L)
(L,x,a) is non empty directed Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in x & b₂ in a ) } is set
downarrow (L,x,a) is non empty directed lower Element of K32( the carrier of L)
b is Element of the carrier of (InclPoset (Ids L))
b "\/" b is Element of the carrier of (InclPoset (Ids L))
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in D1 or b₁ in D2 or ex b₂, b₃ being Element of the carrier of L st
( b₂ in D1 & b₃ in D2 & b₁ = b₂ "\/" b₃ ) ) } is set
{D1,D2} is Element of K32( the carrier of (InclPoset (Ids L)))
K32( the carrier of (InclPoset (Ids L))) is set
B1 is Element of K32( the carrier of L)
downarrow B1 is lower Element of K32( the carrier of L)
b1 is set
A1 is Element of the carrier of L
a1 is Element of the carrier of L
A1 "\/" a1 is Element of the carrier of L
L is non empty RelStr
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
K32( the carrier of [:L,L:]) is set
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of [:L,L:])
proj2 D1 is Element of K32( the carrier of L)
proj1 D1 is Element of K32( the carrier of L)
{ b₁ where b₁ is Element of K32( the carrier of L) : ex b₂ being Element of the carrier of L st
( b₁ = (L,{b₂},(proj2 D1)) & b₂ in proj1 D1 ) } is set
union { b₁ where b₁ is Element of K32( the carrier of L) : ex b₂ being Element of the carrier of L st
( b₁ = (L,{b₂},(proj2 D1)) & b₂ in proj1 D1 ) } is set
(L,(proj1 D1),(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in proj1 D1 & b₂ in proj2 D1 ) } is set
{ b₁ where b₁ is Element of K32( the carrier of L) : S₁[b₁] } is set
union { b₁ where b₁ is Element of K32( the carrier of L) : S₁[b₁] } is set
s is set
x is set
a is Element of K32( the carrier of L)
b is Element of the carrier of L
{b} is Element of K32( the carrier of L)
(L,{b},(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {b} & b₂ in proj2 D1 ) } is set
b is Element of the carrier of L
{b} is Element of K32( the carrier of L)
(L,{b},(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {b} & b₂ in proj2 D1 ) } is set
{ (b "\/" b₁) where b₁ is Element of the carrier of L : b₁ in proj2 D1 } is set
B1 is Element of the carrier of L
b "\/" B1 is Element of the carrier of L
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "\/" a is Element of the carrier of L
{x} is Element of K32( the carrier of L)
(L,{x},(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {x} & b₂ in proj2 D1 ) } is set
{ (x "\/" b₁) where b₁ is Element of the carrier of L : b₁ in proj2 D1 } is set
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
downarrow D1 is lower Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
downarrow D2 is lower Element of K32( the carrier of L)
(L,(downarrow D1),(downarrow D2)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in downarrow D1 & b₂ in downarrow D2 ) } is set
downarrow (L,(downarrow D1),(downarrow D2)) is lower Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
downarrow (L,D1,D2) is lower Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,(downarrow D1),(downarrow D2)) ) } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in D2 ) } is set
B1 is Element of the carrier of L
b1 is Element of the carrier of L
b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in D1 ) } is set
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "\/" b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,D1,D2) ) } is set
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
downarrow D1 is lower Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
downarrow D2 is lower Element of K32( the carrier of L)
(L,(downarrow D1),(downarrow D2)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in downarrow D1 & b₂ in downarrow D2 ) } is set
downarrow (L,(downarrow D1),(downarrow D2)) is lower Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
downarrow (L,D1,D2) is lower Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,D1,D2) ) } is set
q is set
s is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,(downarrow D1),(downarrow D2)) ) } is set
K32((downarrow D1)) is set
K32((downarrow D2)) is set
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
uparrow D1 is upper Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
uparrow D2 is upper Element of K32( the carrier of L)
(L,(uparrow D1),(uparrow D2)) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in uparrow D1 & b₂ in uparrow D2 ) } is set
uparrow (L,(uparrow D1),(uparrow D2)) is upper Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
uparrow (L,D1,D2) is upper Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,(uparrow D1),(uparrow D2)) ) } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in D2 ) } is set
B1 is Element of the carrier of L
b1 is Element of the carrier of L
b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in D1 ) } is set
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "\/" b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,D1,D2) ) } is set
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
uparrow D1 is upper Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
uparrow D2 is upper Element of K32( the carrier of L)
(L,(uparrow D1),(uparrow D2)) is upper Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in uparrow D1 & b₂ in uparrow D2 ) } is set
uparrow (L,(uparrow D1),(uparrow D2)) is upper Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
uparrow (L,D1,D2) is upper Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,D1,D2) ) } is set
q is set
s is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,(uparrow D1),(uparrow D2)) ) } is set
K32((uparrow D1)) is set
K32((uparrow D2)) is set
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "/\" x is Element of the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
(L,s,q) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in s & b₂ in q ) } is set
x is set
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
x is set
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
{} L is empty directed filtered Element of K32( the carrier of L)
D1 is Element of K32( the carrier of L)
(L,D1,({} L)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in {} L ) } is set
D2 is set
q is Element of the carrier of L
s is Element of the carrier of L
q "/\" s is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
q is Element of the carrier of L
D1 is Element of K32( the carrier of L)
s is Element of the carrier of L
D2 is Element of K32( the carrier of L)
q "/\" s is Element of the carrier of L
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is set
x is Element of the carrier of L
s is Element of D2
x "/\" s is Element of the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
s is Element of the carrier of L
x is Element of the carrier of L
s "/\" x is Element of the carrier of L
L is non empty reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
(L,D1,D1) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D1 ) } is set
D2 is set
q is non empty Element of K32( the carrier of L)
s is Element of q
s "/\" s is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of K32( the carrier of L)
(L,(L,D1,D2),q) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in (L,D1,D2) & b₂ in q ) } is set
(L,D2,q) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D2 & b₂ in q ) } is set
(L,D1,(L,D2,q)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in (L,D2,q) ) } is set
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
b is Element of the carrier of L
B1 is Element of the carrier of L
b "/\" B1 is Element of the carrier of L
B1 "/\" a is Element of the carrier of L
b "/\" (B1 "/\" a) is Element of the carrier of L
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
b is Element of the carrier of L
B1 is Element of the carrier of L
b "/\" B1 is Element of the carrier of L
x "/\" b is Element of the carrier of L
(x "/\" b) "/\" B1 is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is non empty Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is set
x is set
a is Element of D1
s is Element of D2
a "/\" s is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is directed Element of K32( the carrier of L)
D2 is directed Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
s is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
B1 is Element of the carrier of L
b1 is Element of the carrier of L
B1 "/\" b1 is Element of the carrier of L
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "/\" A1 is Element of the carrier of L
z is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is filtered Element of K32( the carrier of L)
D2 is filtered Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is Element of the carrier of L
s is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
B1 is Element of the carrier of L
b1 is Element of the carrier of L
B1 "/\" b1 is Element of the carrier of L
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "/\" A1 is Element of the carrier of L
z is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is lower Element of K32( the carrier of L)
D2 is lower Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
s is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
B1 is Element of the carrier of L
B1 is Element of the carrier of L
x "/\" x is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
{ (D2 "/\" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "/\" x is Element of the carrier of L
q is set
s is Element of the carrier of L
D2 "/\" s is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D2 \/ q is Element of K32( the carrier of L)
(L,D1,(D2 \/ q)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 \/ q ) } is set
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
(L,D1,q) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in q ) } is set
(L,D1,D2) \/ (L,D1,q) is Element of K32( the carrier of L)
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
L is non empty reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
(L,D2,q) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D2 & b₂ in q ) } is set
D1 \/ (L,D2,q) is Element of K32( the carrier of L)
D1 \/ D2 is Element of K32( the carrier of L)
D1 \/ q is Element of K32( the carrier of L)
(L,(D1 \/ D2),(D1 \/ q)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 \/ D2 & b₂ in D1 \/ q ) } is set
s is set
x is Element of the carrier of L
x "/\" x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is lower Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
D1 \/ D2 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D1 \/ q is Element of K32( the carrier of L)
(L,(D1 \/ D2),(D1 \/ q)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 \/ D2 & b₂ in D1 \/ q ) } is set
(L,D2,q) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D2 & b₂ in q ) } is set
D1 \/ (L,D2,q) is Element of K32( the carrier of L)
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2} ) } is set
D1 "/\" D2 is Element of the carrier of L
{(D1 "/\" D2)} is Element of K32( the carrier of L)
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "/\" x is Element of the carrier of L
q is set
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
q is Element of the carrier of L
{D2,q} is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2,q} ) } is set
D1 "/\" D2 is Element of the carrier of L
D1 "/\" q is Element of the carrier of L
{(D1 "/\" D2),(D1 "/\" q)} is Element of K32( the carrier of L)
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
s is set
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D1},{D2}) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2} ) } is set
D1 "/\" D2 is Element of the carrier of L
{(D1 "/\" D2)} is Element of K32( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
D1 is Element of the carrier of L
{D1} is Element of K32( the carrier of L)
K32( the carrier of L) is set
D2 is Element of the carrier of L
q is Element of the carrier of L
{D2,q} is Element of K32( the carrier of L)
(L,{D1},{D2,q}) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D1} & b₂ in {D2,q} ) } is set
D1 "/\" D2 is Element of the carrier of L
D1 "/\" q is Element of the carrier of L
{(D1 "/\" D2),(D1 "/\" q)} is Element of K32( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
q is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
x is set
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
L is non empty reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
D1 /\ D2 is Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
q is set
s is non empty Element of K32( the carrier of L)
x is Element of s
x "/\" x is Element of the carrier of L
L is non empty reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is lower Element of K32( the carrier of L)
D2 is lower Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
D1 /\ D2 is Element of K32( the carrier of L)
q is set
s is Element of the carrier of L
x is Element of the carrier of L
s "/\" x is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
L is non empty reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
{ (D2 "/\" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
q is set
s is Element of the carrier of L
D2 "/\" s is Element of the carrier of L
q is set
s is non empty Element of K32( the carrier of L)
x is Element of s
D2 "/\" x is Element of the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
q is Element of the carrier of L
{ (D2 "/\" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
s is Element of the carrier of L
D2 "/\" s is Element of the carrier of L
x is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
"\/" (D1,L) is Element of the carrier of L
D2 is Element of the carrier of L
{D2} is Element of K32( the carrier of L)
(L,{D2},D1) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {D2} & b₂ in D1 ) } is set
"\/" ((L,{D2},D1),L) is Element of the carrier of L
D2 "/\" ("\/" (D1,L)) is Element of the carrier of L
{ (D2 "/\" b₁) where b₁ is Element of the carrier of L : b₁ in D1 } is set
q is Element of the carrier of L
s is Element of the carrier of L
D2 "/\" s is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
"/\" ((L,D1,D2),L) is Element of the carrier of L
the Element of D2 is Element of D2
s is Element of the carrier of L
s "/\" the Element of D2 is Element of the carrier of L
x is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of the carrier of L
D2 is Element of the carrier of L
D1 "/\" D2 is Element of the carrier of L
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of the carrier of L
D2 is Element of the carrier of L
D1 "/\" D2 is Element of the carrier of L
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() up-complete /\-complete RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is non empty Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is non empty Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
"/\" ((L,D1,D2),L) is Element of the carrier of L
"/\" (D1,L) is Element of the carrier of L
"/\" (D2,L) is Element of the carrier of L
("/\" (D1,L)) "/\" ("/\" (D2,L)) is Element of the carrier of L
("/\" ((L,D1,D2),L)) "/\" ("/\" ((L,D1,D2),L)) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
Ids L is non empty set
the carrier of L is non empty set
K32( the carrier of L) is set
{ b₁ where b₁ is non empty directed lower Element of K32( the carrier of L) : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_infima RelStr
the carrier of (InclPoset (Ids L)) is non empty set
D1 is Element of the carrier of (InclPoset (Ids L))
D2 is Element of the carrier of (InclPoset (Ids L))
D1 "/\" D2 is Element of the carrier of (InclPoset (Ids L))
q is Element of K32( the carrier of L)
s is Element of K32( the carrier of L)
(L,q,s) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in q & b₂ in s ) } is set
D1 /\ D2 is set
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
D2 is non empty Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
uparrow (L,D1,D2) is Element of K32( the carrier of L)
q is set
x is set
a is non empty Element of K32( the carrier of L)
b is Element of a
s is Element of D2
b "/\" s is Element of the carrier of L
B1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,D1,D2) ) } is set
(L,a,D2) is non empty Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in a & b₂ in D2 ) } is set
L is non empty RelStr
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
K32( the carrier of [:L,L:]) is set
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of [:L,L:])
proj2 D1 is Element of K32( the carrier of L)
proj1 D1 is Element of K32( the carrier of L)
{ b₁ where b₁ is Element of K32( the carrier of L) : ex b₂ being Element of the carrier of L st
( b₁ = (L,{b₂},(proj2 D1)) & b₂ in proj1 D1 ) } is set
union { b₁ where b₁ is Element of K32( the carrier of L) : ex b₂ being Element of the carrier of L st
( b₁ = (L,{b₂},(proj2 D1)) & b₂ in proj1 D1 ) } is set
(L,(proj1 D1),(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in proj1 D1 & b₂ in proj2 D1 ) } is set
{ b₁ where b₁ is Element of K32( the carrier of L) : S₁[b₁] } is set
union { b₁ where b₁ is Element of K32( the carrier of L) : S₁[b₁] } is set
s is set
x is set
a is Element of K32( the carrier of L)
b is Element of the carrier of L
{b} is Element of K32( the carrier of L)
(L,{b},(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {b} & b₂ in proj2 D1 ) } is set
b is Element of the carrier of L
{b} is Element of K32( the carrier of L)
(L,{b},(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {b} & b₂ in proj2 D1 ) } is set
{ (b "/\" b₁) where b₁ is Element of the carrier of L : b₁ in proj2 D1 } is set
B1 is Element of the carrier of L
b "/\" B1 is Element of the carrier of L
s is set
x is Element of the carrier of L
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
{x} is Element of K32( the carrier of L)
(L,{x},(proj2 D1)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in {x} & b₂ in proj2 D1 ) } is set
{ (x "/\" b₁) where b₁ is Element of the carrier of L : b₁ in proj2 D1 } is set
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
downarrow D1 is lower Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
downarrow D2 is lower Element of K32( the carrier of L)
(L,(downarrow D1),(downarrow D2)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in downarrow D1 & b₂ in downarrow D2 ) } is set
downarrow (L,(downarrow D1),(downarrow D2)) is lower Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
downarrow (L,D1,D2) is lower Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,(downarrow D1),(downarrow D2)) ) } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in D2 ) } is set
B1 is Element of the carrier of L
b1 is Element of the carrier of L
b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in D1 ) } is set
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "/\" b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,D1,D2) ) } is set
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
downarrow D1 is lower Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
downarrow D2 is lower Element of K32( the carrier of L)
(L,(downarrow D1),(downarrow D2)) is lower Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in downarrow D1 & b₂ in downarrow D2 ) } is set
downarrow (L,(downarrow D1),(downarrow D2)) is lower Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
downarrow (L,D1,D2) is lower Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,D1,D2) ) } is set
q is set
s is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in (L,(downarrow D1),(downarrow D2)) ) } is set
K32((downarrow D1)) is set
K32((downarrow D2)) is set
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
uparrow D1 is upper Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
uparrow D2 is upper Element of K32( the carrier of L)
(L,(uparrow D1),(uparrow D2)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in uparrow D1 & b₂ in uparrow D2 ) } is set
uparrow (L,(uparrow D1),(uparrow D2)) is upper Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
uparrow (L,D1,D2) is upper Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,(uparrow D1),(uparrow D2)) ) } is set
q is set
s is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in D2 ) } is set
B1 is Element of the carrier of L
b1 is Element of the carrier of L
b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in D1 ) } is set
A1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 is Element of the carrier of L
a1 "/\" b1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,D1,D2) ) } is set
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is set
D1 is Element of K32( the carrier of L)
uparrow D1 is upper Element of K32( the carrier of L)
D2 is Element of K32( the carrier of L)
uparrow D2 is upper Element of K32( the carrier of L)
(L,(uparrow D1),(uparrow D2)) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in uparrow D1 & b₂ in uparrow D2 ) } is set
uparrow (L,(uparrow D1),(uparrow D2)) is upper Element of K32( the carrier of L)
(L,D1,D2) is Element of K32( the carrier of L)
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of L : ( b₁ in D1 & b₂ in D2 ) } is set
uparrow (L,D1,D2) is upper Element of K32( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,D1,D2) ) } is set
q is set
s is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in (L,(uparrow D1),(uparrow D2)) ) } is set
K32((uparrow D1)) is set
K32((uparrow D2)) is set
x is Element of the carrier of L
x is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L