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

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

(L,s,q) is Element of K32( the carrier of L)

{ (b

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

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

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

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

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

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

q is Element of K32( the carrier of L)

(L,(L,D1,D2),q) is Element of K32( the carrier of L)

{ (b

(L,D2,q) is Element of K32( the carrier of L)

{ (b

(L,D1,(L,D2,q)) is Element of K32( the carrier of L)

{ (b

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

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

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

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

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

{ (D2 "\/" b

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

(L,D1,D2) is Element of K32( the carrier of L)

{ (b

(L,D1,q) is Element of K32( the carrier of L)

{ (b

(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

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

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

(L,D2,q) is Element of K32( the carrier of L)

{ (b

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

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

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

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

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

(L,q,s) is Element of K32( the carrier of L)

{ (b

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

{ (D2 "\/" b

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

q is Element of the carrier of L

{ (D2 "\/" b

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

D2 "\/" ("/\" (D1,L)) is Element of the carrier of L

"/\" ((L,{D2},D1),L) is Element of the carrier of L

{ (D2 "\/" b

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

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

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

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

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

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

( b

(L,a,D2) is non empty Element of K32( the carrier of L)

{ (b

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

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

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

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

( b

{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

( b

union { b

( b

(L,(proj1 D1),(proj2 D1)) is Element of K32( the carrier of L)

{ (b

{ b

union { b

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

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

{ (x "\/" b

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

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

downarrow (L,D1,D2) is lower Element of K32( the carrier of L)

{ b

( b

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

( b

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

( b

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

( b

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

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

downarrow (L,D1,D2) is lower Element of K32( the carrier of L)

{ b

( b

q is set

s is Element of the carrier of L

{ b

( b

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

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

uparrow (L,D1,D2) is upper Element of K32( the carrier of L)

{ b

( b

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

( b

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

( b

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

( b

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

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

uparrow (L,D1,D2) is upper Element of K32( the carrier of L)

{ b

( b

q is set

s is Element of the carrier of L

{ b

( b

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

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

(L,s,q) is Element of K32( the carrier of L)

{ (b

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

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

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

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

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

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

q is Element of K32( the carrier of L)

(L,(L,D1,D2),q) is Element of K32( the carrier of L)

{ (b

(L,D2,q) is Element of K32( the carrier of L)

{ (b

(L,D1,(L,D2,q)) is Element of K32( the carrier of L)

{ (b

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

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

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

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

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

{ (D2 "/\" b

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

(L,D1,D2) is Element of K32( the carrier of L)

{ (b

(L,D1,q) is Element of K32( the carrier of L)

{ (b

(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

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

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

(L,D2,q) is Element of K32( the carrier of L)

{ (b

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

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

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

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

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

(L,q,s) is Element of K32( the carrier of L)

{ (b

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

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

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

{ (D2 "/\" b

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

q is Element of the carrier of L

{ (D2 "/\" b

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

"\/" ((L,{D2},D1),L) is Element of the carrier of L

D2 "/\" ("\/" (D1,L)) is Element of the carrier of L

{ (D2 "/\" b

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

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

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

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

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

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

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

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

( b

(L,a,D2) is non empty Element of K32( the carrier of L)

{ (b

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

( b

union { b

( b

(L,(proj1 D1),(proj2 D1)) is Element of K32( the carrier of L)

{ (b

{ b

union { b

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

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

{ (x "/\" b

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

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

downarrow (L,D1,D2) is lower Element of K32( the carrier of L)

{ b

( b

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

( b

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

( b

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

( b

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

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

downarrow (L,D1,D2) is lower Element of K32( the carrier of L)

{ b

( b

q is set

s is Element of the carrier of L

{ b

( b

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

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

uparrow (L,D1,D2) is upper Element of K32( the carrier of L)

{ b

( b

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

( b

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

( b

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

( b

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

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

uparrow (L,D1,D2) is upper Element of K32( the carrier of L)

{ b

( b

q is set

s is Element of the carrier of L

{ b

( b

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