:: 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
is non empty Element of K32(NAT)
L is set
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
is non empty Element of K32(NAT)
L is set
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

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

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

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

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

the carrier of x is non empty set

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
c15 is Element of the carrier of X2
c19 is non empty Element of K32(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)

the carrier of () 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

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 ()
c15 is Element of the carrier of ()
f is set
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
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))
c19 is Element of the carrier of ()
f . c19 is Element of the carrier of X2
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
c19 is set
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
c19 is set
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 . c15 is Element of the carrier of X2
f . X1 is Element of the carrier of X2
c19 is Element of the carrier of ()
y is Element of the carrier of ()
f . c19 is Element of the carrier of X2
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 . c15 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
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 . c15 is Element of the carrier of X2
the carrier of () is non empty set

the carrier of x is non empty set

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
c15 is Element of the carrier of X2
c19 is non empty Element of K32(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)

the carrier of () 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

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 ()
c15 is Element of the carrier of ()
f is set
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
f is Element of the carrier of x
c19 is Element of the carrier of ()
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))
c19 is Element of the carrier of ()
f . c19 is Element of the carrier of X2
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
c19 is set
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
c19 is set
f . z is Element of the carrier of X2
f . c15 is Element of the carrier of X2
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
c19 is Element of the carrier of ()
y is Element of the carrier of ()
f . c19 is Element of the carrier of X2
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 . c15 is Element of the carrier of X2
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

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

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

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

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

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