:: YELLOW11 semantic presentation

REAL is set

NAT is non empty V27() V28() V29() Element of K32(REAL)

K32(REAL) is non empty set

NAT is non empty V27() V28() V29() set

K32(NAT) is non empty set

{} is empty V27() V28() V29() V31() V32() V33() set

the empty V27() V28() V29() V31() V32() V33() set is empty V27() V28() V29() V31() V32() V33() set

1 is non empty V18() V27() V28() V29() V33() Element of NAT

{{},1} is non empty set

K32(NAT) is non empty set

{{}} is non empty set

2 is non empty V18() V27() V28() V29() V33() Element of NAT

3 is non empty V18() V27() V28() V29() V33() Element of NAT

{{},1,2} is non empty set

0 is empty V27() V28() V29() V31() V32() V33() Element of NAT

{0,1,2} is non empty Element of K32(NAT)

2 \ 1 is Element of K32(2)

K32(2) is non empty set

{1} is non empty Element of K32(NAT)

L is set

{0} is non empty Element of K32(NAT)

L is set

{0} is non empty Element of K32(NAT)

{0,1} is non empty Element of K32(NAT)

3 \ 1 is Element of K32(3)

K32(3) is non empty set

{1,2} is non empty Element of K32(NAT)

L is set

{0} is non empty Element of K32(NAT)

L is set

{0} is non empty Element of K32(NAT)

3 \ 2 is Element of K32(3)

{2} is non empty Element of K32(NAT)

L is set

{0,1} is non empty Element of K32(NAT)

L is set

{0,1} is non empty Element of K32(NAT)

L is set

L is non empty V58() reflexive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "\/" B is Element of the carrier of L

L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

x "/\" B is Element of the carrier of L

y is Element of the carrier of L

x "/\" y is Element of the carrier of L

(x "/\" B) "\/" (x "/\" y) is Element of the carrier of L

B "\/" y is Element of the carrier of L

x "/\" (B "\/" y) is Element of the carrier of L

L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

B "/\" y is Element of the carrier of L

x "\/" (B "/\" y) is Element of the carrier of L

x "\/" B is Element of the carrier of L

x "\/" y is Element of the carrier of L

(x "\/" B) "/\" (x "\/" y) is Element of the carrier of L

L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

y is Element of the carrier of L

B is Element of the carrier of L

B "/\" y is Element of the carrier of L

x "\/" (B "/\" y) is Element of the carrier of L

x "\/" B is Element of the carrier of L

(x "\/" B) "/\" y is Element of the carrier of L

{0,(3 \ 1),2,(3 \ 2),3} is non empty set

InclPoset {0,(3 \ 1),2,(3 \ 2),3} is non empty strict V58() reflexive transitive antisymmetric RelStr

() is RelStr

the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) is non empty set

B is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

y is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

(3 \ 1) /\ 3 is Element of K32(3)

3 /\ 3 is set

(3 /\ 3) \ 1 is Element of K32((3 /\ 3))

K32((3 /\ 3)) is non empty set

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

2 /\ (3 \ 2) is Element of K32(3)

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

2 /\ (3 \ 2) is Element of K32(3)

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

(3 \ 2) /\ 3 is Element of K32(3)

3 /\ 3 is set

(3 /\ 3) \ 2 is Element of K32((3 /\ 3))

K32((3 /\ 3)) is non empty set

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

(3 \ 1) /\ 3 is Element of K32(3)

3 /\ 3 is set

(3 /\ 3) \ 1 is Element of K32((3 /\ 3))

K32((3 /\ 3)) is non empty set

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

(3 \ 2) /\ 3 is Element of K32(3)

3 /\ 3 is set

(3 /\ 3) \ 2 is Element of K32((3 /\ 3))

K32((3 /\ 3)) is non empty set

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B /\ y is set

a is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3})

B is set

y is set

2 \/ 3 is non empty set

2 \/ (3 \ 2) is non empty set

(3 \ 1) \/ 2 is non empty set

{0,1,1,2} is non empty Element of K32(NAT)

{1,1,0,2} is non empty Element of K32(NAT)

{1,0,2} is non empty Element of K32(NAT)

(3 \ 1) \/ 3 is non empty set

(3 \ 2) \/ 3 is non empty set

(3 \ 1) \/ (3 \ 2) is Element of K32(3)

B \/ y is set

{0,1,(2 \ 1),(3 \ 2),3} is non empty set

InclPoset {0,1,(2 \ 1),(3 \ 2),3} is non empty strict V58() reflexive transitive antisymmetric RelStr

() is RelStr

the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3}) is non empty set

B is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

y is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is set

b is set

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is set

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is set

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is set

b is set

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is set

b is set

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is set

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is set

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is set

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is set

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

a is set

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B \/ y is set

a is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

b is Element of the carrier of (InclPoset {0,1,(2 \ 1),(3 \ 2),3})

B is set

(2 \ 1) /\ (3 \ 2) is Element of K32(3)

(3 \ 2) /\ 3 is Element of K32(3)

B is set

(2 \ 1) /\ 3 is Element of K32(2)

1 /\ 3 is set

B is set

1 /\ (3 \ 2) is Element of K32(3)

1 /\ (2 \ 1) is Element of K32(2)

B is set

y is set

B /\ y is set

the carrier of () is non empty set

x is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of x is non empty set

x1 is V58() reflexive transitive antisymmetric full meet-inheriting join-inheriting SubRelStr of x

the carrier of x1 is set

K33( the carrier of (), the carrier of x1) is set

K32(K33( the carrier of (), the carrier of x1)) is non empty set

x2 is V7() V10( the carrier of ()) V11( the carrier of x1) Function-like V21( the carrier of (), the carrier of x1) Element of K32(K33( the carrier of (), the carrier of x1))

X2 is non empty SubRelStr of x

the carrier of X2 is non empty set

X1 is non empty set

rng x2 is Element of K32( the carrier of x1)

K32( the carrier of x1) is non empty set

K33( the carrier of (),X1) is non empty set

K32(K33( the carrier of (),X1)) is non empty set

f1X1 is V7() V10( the carrier of ()) V11(X1) Function-like V21( the carrier of (),X1) Element of K32(K33( the carrier of (),X1))

f1 is Element of the carrier of ()

f1X1 . f1 is Element of X1

B is Element of the carrier of ()

f1X1 . B is Element of X1

y is Element of the carrier of ()

f1X1 . y is Element of X1

b is Element of the carrier of ()

f1X1 . b is Element of X1

a is Element of the carrier of ()

f1X1 . a is Element of X1

c is non empty set

K32(c) is non empty set

c

c

z is Element of the carrier of X2

f is Element of the carrier of X2

f is Element of the carrier of X2

f1X2 is Element of the carrier of X2

y is Element of the carrier of x

X is Element of the carrier of x

y "/\" X is Element of the carrier of x

C is Element of the carrier of x

y "/\" C is Element of the carrier of x

X "/\" C is Element of the carrier of x

X "\/" C is Element of the carrier of x

D is Element of the carrier of x

X "/\" D is Element of the carrier of x

C "/\" D is Element of the carrier of x

C "\/" D is Element of the carrier of x

E is Element of the carrier of x

C "/\" E is Element of the carrier of x

D "/\" E is Element of the carrier of x

x2 . B is Element of the carrier of x1

x2 . y is Element of the carrier of x1

x2 . b is Element of the carrier of x1

x2 . a is Element of the carrier of x1

{X,C} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

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

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{C,D} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

"/\" ({C,D},x) is Element of the carrier of x

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{X,C} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

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

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{C,D} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

"\/" ({C,D},x) is Element of the carrier of x

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

B is Element of the carrier of x

y is Element of the carrier of x

a is Element of the carrier of x

b is Element of the carrier of x

c is Element of the carrier of x

B "/\" y is Element of the carrier of x

B "/\" a is Element of the carrier of x

a "/\" c is Element of the carrier of x

b "/\" c is Element of the carrier of x

y "/\" a is Element of the carrier of x

y "/\" b is Element of the carrier of x

a "/\" b is Element of the carrier of x

y "\/" a is Element of the carrier of x

a "\/" b is Element of the carrier of x

{B,y,a,b,c} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

x1 is Element of K32( the carrier of x)

subrelstr x1 is strict V58() reflexive transitive antisymmetric full SubRelStr of x

the carrier of (subrelstr x1) is set

X2 is Element of the carrier of x

X1 is Element of the carrier of x

{X2,X1} is non empty Element of K32( the carrier of x)

"/\" ({X2,X1},x) is Element of the carrier of x

B "/\" B is Element of the carrier of x

B "/\" b is Element of the carrier of x

B "/\" c is Element of the carrier of x

y "/\" y is Element of the carrier of x

y "/\" c is Element of the carrier of x

a "/\" a is Element of the carrier of x

B "/\" b is Element of the carrier of x

b "/\" b is Element of the carrier of x

B "/\" c is Element of the carrier of x

y "/\" c is Element of the carrier of x

c "/\" c is Element of the carrier of x

X2 is Element of the carrier of x

X1 is Element of the carrier of x

{X2,X1} is non empty Element of K32( the carrier of x)

"\/" ({X2,X1},x) is Element of the carrier of x

B "\/" B is Element of the carrier of x

X2 "\/" X1 is Element of the carrier of x

X2 "\/" X1 is Element of the carrier of x

B "/\" b is Element of the carrier of x

B "\/" b is Element of the carrier of x

B "/\" c is Element of the carrier of x

B "\/" c is Element of the carrier of x

B "\/" y is Element of the carrier of x

y "\/" y is Element of the carrier of x

y "\/" b is Element of the carrier of x

y "/\" c is Element of the carrier of x

y "\/" c is Element of the carrier of x

a "\/" B is Element of the carrier of x

a "\/" a is Element of the carrier of x

a "\/" c is Element of the carrier of x

B "/\" b is Element of the carrier of x

B "\/" b is Element of the carrier of x

y "\/" b is Element of the carrier of x

b "\/" b is Element of the carrier of x

b "\/" c is Element of the carrier of x

B "/\" c is Element of the carrier of x

B "\/" c is Element of the carrier of x

y "/\" c is Element of the carrier of x

y "\/" c is Element of the carrier of x

a "\/" c is Element of the carrier of x

b "\/" c is Element of the carrier of x

c "\/" c is Element of the carrier of x

X2 is non empty V58() reflexive transitive antisymmetric with_suprema with_infima full meet-inheriting join-inheriting SubRelStr of x

f1X2 is Element of the carrier of ()

f1X1 is Element of the carrier of ()

X1 is Element of the carrier of ()

z is Element of the carrier of ()

c

f is set

f is Element of the carrier of x

c

f is Element of the carrier of x

c

f is Element of the carrier of x

c

f is Element of the carrier of x

c

f is Element of the carrier of x

c

K33( the carrier of (),x1) is set

K32(K33( the carrier of (),x1)) is non empty set

f is V7() V10( the carrier of ()) V11(x1) Function-like V21( the carrier of (),x1) Element of K32(K33( the carrier of (),x1))

the carrier of X2 is non empty set

K33( the carrier of (), the carrier of X2) is non empty set

K32(K33( the carrier of (), the carrier of X2)) is non empty set

f is V7() V10( the carrier of ()) V11( the carrier of X2) Function-like V21( the carrier of (), the carrier of X2) Element of K32(K33( the carrier of (), the carrier of X2))

c

f . c

y is Element of the carrier of ()

f . y is Element of the carrier of X2

rng f is Element of K32( the carrier of X2)

K32( the carrier of X2) is non empty set

c

dom f is Element of K32( the carrier of ())

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

y is set

f . y is set

X is Element of the carrier of ()

dom f is Element of K32( the carrier of ())

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

c

f . z is Element of the carrier of X2

f . f1X1 is Element of the carrier of X2

f . f1X2 is Element of the carrier of X2

f . c

f . X1 is Element of the carrier of X2

c

y is Element of the carrier of ()

f . c

f . y is Element of the carrier of X2

f . z is Element of the carrier of X2

f . z is Element of the carrier of X2

f . z is Element of the carrier of X2

f . z is Element of the carrier of X2

f . c

f . f1X1 is Element of the carrier of X2

f . X1 is Element of the carrier of X2

f . f1X1 is Element of the carrier of X2

X is set

f . X1 is Element of the carrier of X2

f . f1X2 is Element of the carrier of X2

f . X1 is Element of the carrier of X2

f . c

the carrier of () is non empty set

x is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of x is non empty set

x1 is V58() reflexive transitive antisymmetric full meet-inheriting join-inheriting SubRelStr of x

the carrier of x1 is set

K33( the carrier of (), the carrier of x1) is set

K32(K33( the carrier of (), the carrier of x1)) is non empty set

x2 is V7() V10( the carrier of ()) V11( the carrier of x1) Function-like V21( the carrier of (), the carrier of x1) Element of K32(K33( the carrier of (), the carrier of x1))

X2 is non empty SubRelStr of x

the carrier of X2 is non empty set

X1 is non empty set

rng x2 is Element of K32( the carrier of x1)

K32( the carrier of x1) is non empty set

K33( the carrier of (),X1) is non empty set

K32(K33( the carrier of (),X1)) is non empty set

f1X1 is V7() V10( the carrier of ()) V11(X1) Function-like V21( the carrier of (),X1) Element of K32(K33( the carrier of (),X1))

f1 is Element of the carrier of ()

f1X1 . f1 is Element of X1

b is Element of the carrier of ()

f1X1 . b is Element of X1

y is Element of the carrier of ()

f1X1 . y is Element of X1

B is Element of the carrier of ()

f1X1 . B is Element of X1

a is Element of the carrier of ()

f1X1 . a is Element of X1

c is non empty set

K32(c) is non empty set

c

c

z is Element of the carrier of X2

f is Element of the carrier of X2

f is Element of the carrier of X2

f1X2 is Element of the carrier of X2

y is Element of the carrier of x

X is Element of the carrier of x

y "/\" X is Element of the carrier of x

C is Element of the carrier of x

y "/\" C is Element of the carrier of x

X "/\" C is Element of the carrier of x

X "\/" C is Element of the carrier of x

D is Element of the carrier of x

y "/\" D is Element of the carrier of x

X "/\" D is Element of the carrier of x

C "/\" D is Element of the carrier of x

X "\/" D is Element of the carrier of x

C "\/" D is Element of the carrier of x

E is Element of the carrier of x

X "/\" E is Element of the carrier of x

C "/\" E is Element of the carrier of x

D "/\" E is Element of the carrier of x

x2 . b is Element of the carrier of x1

x2 . y is Element of the carrier of x1

x2 . B is Element of the carrier of x1

x2 . a is Element of the carrier of x1

x is set

{X,C} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

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

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{X,D} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

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

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{C,D} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

"/\" ({C,D},x) is Element of the carrier of x

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{X,C} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

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

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{X,D} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

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

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

{C,D} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

"\/" ({C,D},x) is Element of the carrier of x

dom x2 is Element of K32( the carrier of ())

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

x is set

x2 . x is set

B is Element of the carrier of x

y is Element of the carrier of x

a is Element of the carrier of x

b is Element of the carrier of x

c is Element of the carrier of x

B "/\" y is Element of the carrier of x

B "/\" a is Element of the carrier of x

B "/\" b is Element of the carrier of x

y "/\" c is Element of the carrier of x

a "/\" c is Element of the carrier of x

b "/\" c is Element of the carrier of x

y "/\" a is Element of the carrier of x

y "/\" b is Element of the carrier of x

a "/\" b is Element of the carrier of x

y "\/" a is Element of the carrier of x

y "\/" b is Element of the carrier of x

a "\/" b is Element of the carrier of x

{B,y,a,b,c} is non empty Element of K32( the carrier of x)

K32( the carrier of x) is non empty set

x1 is Element of K32( the carrier of x)

subrelstr x1 is strict V58() reflexive transitive antisymmetric full SubRelStr of x

the carrier of (subrelstr x1) is set

X2 is Element of the carrier of x

X1 is Element of the carrier of x

{X2,X1} is non empty Element of K32( the carrier of x)

"/\" ({X2,X1},x) is Element of the carrier of x

B "/\" B is Element of the carrier of x

B "/\" c is Element of the carrier of x

y "/\" y is Element of the carrier of x

a "/\" a is Element of the carrier of x

b "/\" b is Element of the carrier of x

B "/\" c is Element of the carrier of x

c "/\" c is Element of the carrier of x

X2 is Element of the carrier of x

X1 is Element of the carrier of x

{X2,X1} is non empty Element of K32( the carrier of x)

"\/" ({X2,X1},x) is Element of the carrier of x

B "\/" B is Element of the carrier of x

X2 "\/" X1 is Element of the carrier of x

X2 "\/" X1 is Element of the carrier of x

X2 "\/" X1 is Element of the carrier of x

B "/\" c is Element of the carrier of x

B "\/" c is Element of the carrier of x

B "\/" y is Element of the carrier of x

y "\/" y is Element of the carrier of x

y "\/" c is Element of the carrier of x

a "\/" B is Element of the carrier of x

a "\/" a is Element of the carrier of x

a "\/" c is Element of the carrier of x

X2 "\/" X1 is Element of the carrier of x

b "\/" b is Element of the carrier of x

b "\/" c is Element of the carrier of x

B "/\" c is Element of the carrier of x

B "\/" c is Element of the carrier of x

y "\/" c is Element of the carrier of x

a "\/" c is Element of the carrier of x

b "\/" c is Element of the carrier of x

c "\/" c is Element of the carrier of x

X2 is non empty V58() reflexive transitive antisymmetric with_suprema with_infima full meet-inheriting join-inheriting SubRelStr of x

X1 is Element of the carrier of ()

f1X2 is Element of the carrier of ()

f1X1 is Element of the carrier of ()

z is Element of the carrier of ()

c

f is set

f is Element of the carrier of x

c

f is Element of the carrier of x

c

f is Element of the carrier of x

c

f is Element of the carrier of x

c

f is Element of the carrier of x

c

K33( the carrier of (),x1) is set

K32(K33( the carrier of (),x1)) is non empty set

f is V7() V10( the carrier of ()) V11(x1) Function-like V21( the carrier of (),x1) Element of K32(K33( the carrier of (),x1))

the carrier of X2 is non empty set

K33( the carrier of (), the carrier of X2) is non empty set

K32(K33( the carrier of (), the carrier of X2)) is non empty set

f is V7() V10( the carrier of ()) V11( the carrier of X2) Function-like V21( the carrier of (), the carrier of X2) Element of K32(K33( the carrier of (), the carrier of X2))

c

f . c

y is Element of the carrier of ()

f . y is Element of the carrier of X2

rng f is Element of K32( the carrier of X2)

K32( the carrier of X2) is non empty set

c

dom f is Element of K32( the carrier of ())

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

y is set

f . y is set

X is Element of the carrier of ()

dom f is Element of K32( the carrier of ())

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

c

f . z is Element of the carrier of X2

f . c

f . f1X2 is Element of the carrier of X2

f . f1X1 is Element of the carrier of X2

f . X1 is Element of the carrier of X2

c

y is Element of the carrier of ()

f . c

f . y is Element of the carrier of X2

X is set

f . z is Element of the carrier of X2

f . z is Element of the carrier of X2

f . z is Element of the carrier of X2

f . z is Element of the carrier of X2

f . X1 is Element of the carrier of X2

f . c

f . X1 is Element of the carrier of X2

f . f1X2 is Element of the carrier of X2

f . X1 is Element of the carrier of X2

f . f1X1 is Element of the carrier of X2

L is non empty V58() reflexive antisymmetric with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

y is Element of the carrier of L

B is Element of the carrier of L

B "/\" y is Element of the carrier of L

x "\/" (B "/\" y) is Element of the carrier of L

x "/\" y is Element of the carrier of L

(x "/\" y) "\/" (B "/\" y) is Element of the carrier of L

x "\/" B is Element of the carrier of L

(x "\/" B) "/\" y is Element of the carrier of L

L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

y "\/" a is Element of the carrier of L

B "\/" (y "/\" a) is Element of the carrier of L

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

y "\/" a is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

B is Element of the carrier of L

B "/\" y is Element of the carrier of L

x "\/" (B "/\" y) is Element of the carrier of L

x "\/" B is Element of the carrier of L

(x "\/" B) "/\" y is Element of the carrier of L

y "\/" (B "/\" y) is Element of the carrier of L

(x "\/" B) "/\" x is Element of the carrier of L

((x "\/" B) "/\" y) "\/" B is Element of the carrier of L

(x "\/" (B "/\" y)) "/\" B is Element of the carrier of L

y "/\" y is Element of the carrier of L

B "/\" (y "/\" y) is Element of the carrier of L

x "\/" x is Element of the carrier of L

(x "\/" x) "\/" B is Element of the carrier of L

(B "/\" y) "/\" (B "/\" y) is Element of the carrier of L

x2 is Element of the carrier of L

X2 is Element of the carrier of L

x2 "/\" X2 is Element of the carrier of L

X1 is Element of the carrier of L

x2 "/\" X1 is Element of the carrier of L

X2 "/\" X1 is Element of the carrier of L

X2 "\/" X1 is Element of the carrier of L

f1X1 is Element of the carrier of L

X2 "/\" f1X1 is Element of the carrier of L

X1 "/\" f1X1 is Element of the carrier of L

X1 "\/" f1X1 is Element of the carrier of L

f1X2 is Element of the carrier of L

X1 "/\" f1X2 is Element of the carrier of L

f1X1 "/\" f1X2 is Element of the carrier of L

(B "/\" y) "\/" B is Element of the carrier of L

x "\/" ((B "/\" y) "\/" B) is Element of the carrier of L

(x "\/" B) "/\" B is Element of the carrier of L

((x "\/" B) "/\" B) "/\" y is Element of the carrier of L

f1X1 "\/" X1 is Element of the carrier of L

f1X1 "/\" X1 is Element of the carrier of L

x "/\" x is Element of the carrier of L

B "/\" (x "\/" B) is Element of the carrier of L

(B "/\" (x "\/" B)) "/\" y is Element of the carrier of L

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

y "\/" a is Element of the carrier of L

L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

y "\/" a is Element of the carrier of L

x is V58() reflexive transitive antisymmetric full meet-inheriting join-inheriting SubRelStr of L

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

y "\/" a is Element of the carrier of L

L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

x "/\" a is Element of the carrier of L

B "/\" b is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

B "\/" a is Element of the carrier of L

y "\/" a is Element of the carrier of L

(B "/\" y) "\/" (B "/\" a) is Element of the carrier of L

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

x "/\" a is Element of the carrier of L

B "/\" b is Element of the carrier of L

y "/\" b is Element of the carrier of L

a "/\" b is Element of the carrier of L

B "/\" y is Element of the carrier of L

B "/\" a is Element of the carrier of L

y "/\" a is Element of the carrier of L

B "\/" y is Element of the carrier of L

B "\/" a is Element of the carrier of L

y "\/" a is Element of the carrier of L

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

B "\/" y is Element of the carrier of L

x "/\" (B "\/" y) is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is Element of the carrier of L

(x "/\" B) "\/" (x "/\" y) is Element of the carrier of L

x "\/" B is Element of the carrier of L

(x "\/" B) "/\" (B "\/" y) is Element of the carrier of L

y "\/" x is Element of the carrier of L

((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x) is Element of the carrier of L

B "/\" y is Element of the carrier of L

(x "/\" B) "\/" (B "/\" y) is Element of the carrier of L

y "/\" x is Element of the carrier of L

((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x) is Element of the carrier of L

x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

x "/\" ((x "\/" B) "/\" (B "\/" y)) is Element of the carrier of L

(x "/\" ((x "\/" B) "/\" (B "\/" y))) "/\" (y "\/" x) is Element of the carrier of L

x "/\" (x "\/" B) is Element of the carrier of L

(x "/\" (x "\/" B)) "/\" (B "\/" y) is Element of the carrier of L

((x "/\" (x "\/" B)) "/\" (B "\/" y)) "/\" (y "\/" x) is Element of the carrier of L

(x "/\" (B "\/" y)) "/\" (y "\/" x) is Element of the carrier of L

x "/\" (y "\/" x) is Element of the carrier of L

(x "/\" (y "\/" x)) "/\" (B "\/" y) is Element of the carrier of L

(B "/\" y) "/\" x is Element of the carrier of L

((B "/\" y) "/\" x) "\/" (y "/\" x) is Element of the carrier of L

(B "/\" y) "\/" (y "/\" x) is Element of the carrier of L

(x "/\" B) "\/" ((B "/\" y) "\/" (y "/\" x)) is Element of the carrier of L

((x "/\" B) "\/" ((B "/\" y) "\/" (y "/\" x))) "/\" x is Element of the carrier of L

((B "/\" y) "\/" (y "/\" x)) "/\" x is Element of the carrier of L

(x "/\" B) "\/" (((B "/\" y) "\/" (y "/\" x)) "/\" x) is Element of the carrier of L

(x "/\" B) "\/" (y "/\" x) is Element of the carrier of L

B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

(B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

(B "/\" y) "/\" (B "/\" y) is Element of the carrier of L

(y "\/" x) "/\" x is Element of the carrier of L

((y "\/" x) "/\" x) "/\" (B "\/" y) is Element of the carrier of L

y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

(y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

(y "/\" x) "/\" (y "/\" x) is Element of the carrier of L

B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

B "/\" ((x "\/" B) "/\" (B "\/" y)) is Element of the carrier of L

(B "/\" ((x "\/" B) "/\" (B "\/" y))) "/\" (y "\/" x) is Element of the carrier of L

B "/\" (x "\/" B) is Element of the carrier of L

(B "/\" (x "\/" B)) "/\" (B "\/" y) is Element of the carrier of L

((B "/\" (x "\/" B)) "/\" (B "\/" y)) "/\" (y "\/" x) is Element of the carrier of L

B "/\" (B "\/" y) is Element of the carrier of L

(B "/\" (B "\/" y)) "/\" (y "\/" x) is Element of the carrier of L

x "\/" y is Element of the carrier of L

B "/\" (x "\/" y) is Element of the carrier of L

x "\/" (B "/\" y) is Element of the carrier of L

y "\/" (x "/\" B) is Element of the carrier of L

y "\/" B is Element of the carrier of L

(y "\/" x) "/\" (y "\/" B) is Element of the carrier of L

B "\/" (x "/\" y) is Element of the carrier of L

B "\/" x is Element of the carrier of L

(B "\/" x) "/\" (B "\/" y) is Element of the carrier of L

x "/\" (y "\/" B) is Element of the carrier of L

B "\/" ((x "/\" B) "\/" (B "/\" y)) is Element of the carrier of L

(B "\/" ((x "/\" B) "\/" (B "/\" y))) "\/" (y "/\" x) is Element of the carrier of L

B "\/" (x "/\" B) is Element of the carrier of L

(B "\/" (x "/\" B)) "\/" (B "/\" y) is Element of the carrier of L

((B "\/" (x "/\" B)) "\/" (B "/\" y)) "\/" (y "/\" x) is Element of the carrier of L

B "\/" (B "/\" y) is Element of the carrier of L

(B "\/" (B "/\" y)) "\/" (y "/\" x) is Element of the carrier of L

y "/\" B is Element of the carrier of L

x "\/" (y "/\" B) is Element of the carrier of L

B "\/" (y "/\" x) is Element of the carrier of L

(B "\/" y) "/\" (B "\/" x) is Element of the carrier of L

y "/\" (B "\/" x) is Element of the carrier of L

y "\/" (y "/\" x) is Element of the carrier of L

(y "\/" (y "/\" x)) "\/" ((x "/\" B) "\/" (B "/\" y)) is Element of the carrier of L

(B "/\" y) "\/" (x "/\" B) is Element of the carrier of L

y "\/" ((B "/\" y) "\/" (x "/\" B)) is Element of the carrier of L

y "\/" (B "/\" y) is Element of the carrier of L

(y "\/" (B "/\" y)) "\/" (x "/\" B) is Element of the carrier of L

((x "/\" B) "\/" (x "/\" y)) "\/" ((x "/\" B) "\/" (B "/\" y)) is Element of the carrier of L

(x "/\" (B "\/" y)) "\/" (B "/\" (x "\/" y)) is Element of the carrier of L

(x "/\" B) "\/" ((x "/\" B) "\/" (B "/\" y)) is Element of the carrier of L

(x "/\" y) "\/" ((x "/\" B) "\/" ((x "/\" B) "\/" (B "/\" y))) is Element of the carrier of L

(x "/\" B) "\/" (x "/\" B) is Element of the carrier of L

((x "/\" B) "\/" (x "/\" B)) "\/" (B "/\" y) is Element of the carrier of L

(x "/\" y) "\/" (((x "/\" B) "\/" (x "/\" B)) "\/" (B "/\" y)) is Element of the carrier of L

((x "/\" B) "\/" (x "/\" B)) "\/" (x "/\" y) is Element of the carrier of L

(((x "/\" B) "\/" (x "/\" B)) "\/" (x "/\" y)) "\/" (B "/\" y) is Element of the carrier of L

((x "/\" B) "\/" (x "/\" y)) "\/" (B "/\" y) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" ((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

B "/\" x is Element of the carrier of L

y "\/" (B "/\" x) is Element of the carrier of L

x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

x "\/" ((x "/\" B) "\/" (B "/\" y)) is Element of the carrier of L

(x "\/" ((x "/\" B) "\/" (B "/\" y))) "\/" (y "/\" x) is Element of the carrier of L

x "\/" (x "/\" B) is Element of the carrier of L

(x "\/" (x "/\" B)) "\/" (B "/\" y) is Element of the carrier of L

((x "\/" (x "/\" B)) "\/" (B "/\" y)) "\/" (y "/\" x) is Element of the carrier of L

(x "\/" (B "/\" y)) "\/" (y "/\" x) is Element of the carrier of L

(y "/\" x) "\/" x is Element of the carrier of L

((y "/\" x) "\/" x) "\/" (B "/\" y) is Element of the carrier of L

(y "\/" B) "/\" (y "\/" x) is Element of the carrier of L

(y "\/" (B "/\" x)) "/\" (B "\/" (y "/\" x)) is Element of the carrier of L

((y "\/" B) "/\" (y "\/" x)) "/\" ((B "\/" y) "/\" (B "\/" x)) is Element of the carrier of L

(y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

((y "\/" x) "/\" (y "\/" B)) "/\" (y "\/" B) is Element of the carrier of L

(((y "\/" x) "/\" (y "\/" B)) "/\" (y "\/" B)) "/\" (B "\/" x) is Element of the carrier of L

(y "\/" B) "/\" (y "\/" B) is Element of the carrier of L

(y "\/" x) "/\" ((y "\/" B) "/\" (y "\/" B)) is Element of the carrier of L

((y "\/" x) "/\" ((y "\/" B) "/\" (y "\/" B))) "/\" (B "\/" x) is Element of the carrier of L

((y "\/" x) "/\" (y "\/" B)) "/\" (B "\/" x) is Element of the carrier of L

(((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

(x "/\" B) "/\" (x "/\" B) is Element of the carrier of L

y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

y "/\" (y "\/" x) is Element of the carrier of L

(y "/\" (y "\/" x)) "/\" ((x "\/" B) "/\" (B "\/" y)) is Element of the carrier of L

(B "\/" y) "/\" (x "\/" B) is Element of the carrier of L

y "/\" ((B "\/" y) "/\" (x "\/" B)) is Element of the carrier of L

y "/\" (B "\/" y) is Element of the carrier of L

(y "/\" (B "\/" y)) "/\" (x "\/" B) is Element of the carrier of L

y "/\" (x "\/" B) is Element of the carrier of L

(x "\/" B) "/\" (x "\/" y) is Element of the carrier of L

(x "\/" (B "/\" y)) "/\" (B "\/" (x "/\" y)) is Element of the carrier of L

((x "\/" B) "/\" (x "\/" y)) "/\" ((B "\/" x) "/\" (B "\/" y)) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(x "\/" y) "/\" (x "\/" B) is Element of the carrier of L

((x "\/" y) "/\" (x "\/" B)) "/\" (x "\/" B) is Element of the carrier of L

(((x "\/" y) "/\" (x "\/" B)) "/\" (x "\/" B)) "/\" (B "\/" y) is Element of the carrier of L

(x "\/" B) "/\" (x "\/" B) is Element of the carrier of L

(x "\/" y) "/\" ((x "\/" B) "/\" (x "\/" B)) is Element of the carrier of L

((x "\/" y) "/\" ((x "\/" B) "/\" (x "\/" B))) "/\" (B "\/" y) is Element of the carrier of L

((x "\/" y) "/\" (x "\/" B)) "/\" (B "\/" y) is Element of the carrier of L

(y "/\" B) "\/" (B "/\" x) is Element of the carrier of L

B "/\" (y "\/" x) is Element of the carrier of L

((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" ((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) is Element of the carrier of L

(((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

B "/\" (x "\/" (B "/\" y)) is Element of the carrier of L

(B "/\" (x "\/" (B "/\" y))) "\/" (x "/\" y) is Element of the carrier of L

(((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "\/" (y "/\" B)) "/\" (y "\/" (x "/\" B)) is Element of the carrier of L

((x "\/" y) "/\" (x "\/" B)) "/\" ((y "\/" x) "/\" (y "\/" B)) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

((x "\/" B) "/\" (x "\/" y)) "/\" (x "\/" y) is Element of the carrier of L

(((x "\/" B) "/\" (x "\/" y)) "/\" (x "\/" y)) "/\" (y "\/" B) is Element of the carrier of L

(x "\/" y) "/\" (x "\/" y) is Element of the carrier of L

(x "\/" B) "/\" ((x "\/" y) "/\" (x "\/" y)) is Element of the carrier of L

((x "\/" B) "/\" ((x "\/" y) "/\" (x "\/" y))) "/\" (y "\/" B) is Element of the carrier of L

((x "\/" B) "/\" (x "\/" y)) "/\" (y "\/" B) is Element of the carrier of L

(((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" ((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" ((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) is Element of the carrier of L

(y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) is Element of the carrier of L

(y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

B "/\" (y "\/" (B "/\" x)) is Element of the carrier of L

(B "/\" (y "\/" (B "/\" x))) "\/" (y "/\" x) is Element of the carrier of L

(y "/\" B) "\/" (y "/\" x) is Element of the carrier of L

((y "/\" B) "\/" (y "/\" x)) "\/" ((y "/\" B) "\/" (B "/\" x)) is Element of the carrier of L

(y "/\" (B "\/" x)) "\/" (B "/\" (y "\/" x)) is Element of the carrier of L

(y "/\" B) "\/" ((y "/\" B) "\/" (B "/\" x)) is Element of the carrier of L

(y "/\" x) "\/" ((y "/\" B) "\/" ((y "/\" B) "\/" (B "/\" x))) is Element of the carrier of L

(y "/\" B) "\/" (y "/\" B) is Element of the carrier of L

((y "/\" B) "\/" (y "/\" B)) "\/" (B "/\" x) is Element of the carrier of L

(y "/\" x) "\/" (((y "/\" B) "\/" (y "/\" B)) "\/" (B "/\" x)) is Element of the carrier of L

((y "/\" B) "\/" (y "/\" B)) "\/" (y "/\" x) is Element of the carrier of L

(((y "/\" B) "\/" (y "/\" B)) "\/" (y "/\" x)) "\/" (B "/\" x) is Element of the carrier of L

((y "/\" B) "\/" (y "/\" x)) "\/" (B "/\" x) is Element of the carrier of L

(y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "/\" y) "\/" (y "/\" B) is Element of the carrier of L

(x "/\" y) "\/" (x "/\" B) is Element of the carrier of L

((x "/\" y) "\/" (x "/\" B)) "\/" ((x "/\" y) "\/" (y "/\" B)) is Element of the carrier of L

(x "/\" (y "\/" B)) "\/" (y "/\" (x "\/" B)) is Element of the carrier of L

(x "/\" y) "\/" ((x "/\" y) "\/" (y "/\" B)) is Element of the carrier of L

(x "/\" B) "\/" ((x "/\" y) "\/" ((x "/\" y) "\/" (y "/\" B))) is Element of the carrier of L

(x "/\" y) "\/" (x "/\" y) is Element of the carrier of L

((x "/\" y) "\/" (x "/\" y)) "\/" (y "/\" B) is Element of the carrier of L

(x "/\" B) "\/" (((x "/\" y) "\/" (x "/\" y)) "\/" (y "/\" B)) is Element of the carrier of L

((x "/\" y) "\/" (x "/\" y)) "\/" (x "/\" B) is Element of the carrier of L

(((x "/\" y) "\/" (x "/\" y)) "\/" (x "/\" B)) "\/" (y "/\" B) is Element of the carrier of L

((x "/\" y) "\/" (x "/\" B)) "\/" (y "/\" B) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "\/" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

(y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

((x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" ((y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) is Element of the carrier of L

(((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" (y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" (y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

((x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

y "\/" (x "/\" (y "\/" B)) is Element of the carrier of L

(y "\/" (x "/\" (y "\/" B))) "/\" (x "\/" B) is Element of the carrier of L

((y "\/" x) "/\" (y "\/" B)) "/\" (x "\/" B) is Element of the carrier of L

(B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

((x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) is Element of the carrier of L

((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) is Element of the carrier of L

(x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

((x "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

B "\/" (x "/\" (B "\/" y)) is Element of the carrier of L

(B "\/" (x "/\" (B "\/" y))) "/\" (x "\/" y) is Element of the carrier of L

((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((B "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

((y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) is Element of the carrier of L

(y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) is Element of the carrier of L

(y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" ((B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

((y "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "\/" (B "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) is Element of the carrier of L

B "\/" (y "/\" (B "\/" x)) is Element of the carrier of L

(B "\/" (y "/\" (B "\/" x))) "/\" (y "\/" x) is Element of the carrier of L

((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" ((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" ((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" ((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)))) is Element of the carrier of L

((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" (y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) "/\" (y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) is Element of the carrier of L

(x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" ((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x)) is Element of the carrier of L

y "/\" (x "\/" (y "/\" B)) is Element of the carrier of L

(y "/\" (x "\/" (y "/\" B))) "\/" (x "/\" B) is Element of the carrier of L

(y "/\" x) "\/" (y "/\" B) is Element of the carrier of L

((y "/\" x) "\/" (y "/\" B)) "\/" (x "/\" B) is Element of the carrier of L

(((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((y "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

(((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x)) "\/" ((x "\/" (((x "/\" B) "\/" (B "/\" y)) "\/" (y "/\" x))) "/\" (((x "\/" B) "/\" (B "\/" y)) "/\" (y "\/" x))) is Element of the carrier of L

x2 is Element of the carrier of L

X2 is Element of the carrier of L

x2 "/\" X2 is Element of the carrier of L

X1 is Element of the carrier of L

x2 "/\" X1 is Element of the carrier of L

X2 "/\" X1 is Element of the carrier of L

X2 "\/" X1 is Element of the carrier of L

f1X1 is Element of the carrier of L

x2 "/\" f1X1 is Element of the carrier of L

X2 "/\" f1X1 is Element of the carrier of L

X1 "/\" f1X1 is Element of the carrier of L

X2 "\/" f1X1 is Element of the carrier of L

X1 "\/" f1X1 is Element of the carrier of L

f1X2 is Element of the carrier of L

X2 "/\" f1X2 is Element of the carrier of L

X1 "/\" f1X2 is Element of the carrier of L

f1X1 "/\" f1X2 is Element of the carrier of L

x is Element of the carrier of L

B is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

x "/\" B is Element of the carrier of L

x "/\" y is