:: 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₁₅ is Element of the carrier of X2
c₁₉ 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)
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₁₅ is Element of the carrier of ()
f is set
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ 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))
c₁₉ is Element of the carrier of ()
f . c₁₉ 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
c₁₉ 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
c₁₉ 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 . c₁₅ is Element of the carrier of X2
f . X1 is Element of the carrier of X2
c₁₉ is Element of the carrier of ()
y is Element of the carrier of ()
f . c₁₉ 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 . c₁₅ 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 . c₁₅ is Element of the carrier of X2
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₁₅ is Element of the carrier of X2
c₁₉ 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)
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₁₅ is Element of the carrier of ()
f is set
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ is Element of the carrier of ()
f is Element of the carrier of x
c₁₉ 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))
c₁₉ is Element of the carrier of ()
f . c₁₉ 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
c₁₉ 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
c₁₉ is set
f . z is Element of the carrier of X2
f . c₁₅ 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
c₁₉ is Element of the carrier of ()
y is Element of the carrier of ()
f . c₁₉ 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 . c₁₅ 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
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 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
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
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
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
L is non empty RelStr
the carrier of L is non empty set
K32( 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 set
a is set
a is Element of K32( the carrier of L)
b is Element of K32( the carrier of L)
c is Element of the carrier of L
f1 is Element of the carrier of L
y is Element of K32( the carrier of L)
a is Element of K32( the carrier of L)
b is set
c is Element of the carrier of L
b is set
c is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
x is Element of K32( the carrier of L)
B is set
a is Element of the carrier of L
b is Element of the carrier of L
(L,a,b) is Element of K32( the carrier of L)
y is Element of the carrier of L
c is Element of the carrier of L
f1 is Element of the carrier of L
x is Element of K32( the carrier of L)
B is set
a is Element of the carrier of L
b is Element of the carrier of L
(L,a,b) is Element of K32( the carrier of L)
y is Element of the carrier of L
c is Element of the carrier of L
f1 is Element of the carrier of L
L is non empty 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
(L,x,B) is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
L is non empty V58() reflexive transitive 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
(L,x,B) is (L) Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
uparrow x is Element of K32( the carrier of L)
{x} is non empty Element of K32( the carrier of L)
uparrow {x} is Element of K32( the carrier of L)
downarrow B is Element of K32( the carrier of L)
{B} is non empty Element of K32( the carrier of L)
downarrow {B} is Element of K32( the carrier of L)
(uparrow x) /\ (downarrow B) is Element of K32( the carrier of L)
y is set
a is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in {B} ) } is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in {x} ) } is set
y is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in {x} ) } is set
a is Element of the carrier of L
b is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in {B} ) } is set
b is Element of the carrier of L
c is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric 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
(L,x,B) is (L) Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
subrelstr (L,x,B) is strict V58() reflexive transitive antisymmetric full SubRelStr of L
y is Element of the carrier of L
the carrier of (subrelstr (L,x,B)) is set
a is Element of the carrier of L
{y,a} is non empty Element of K32( the carrier of L)
"/\" ({y,a},L) 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 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
(L,x,B) is (L) Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
subrelstr (L,x,B) is strict V58() reflexive transitive antisymmetric full SubRelStr of L
y is Element of the carrier of L
the carrier of (subrelstr (L,x,B)) is set
a is Element of the carrier of L
{y,a} is non empty Element of K32( the carrier of L)
"\/" ({y,a},L) 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
B is Element of the carrier of L
x is Element of the carrier of L
x "\/" B is Element of the carrier of L
(L,B,(x "\/" B)) is (L) Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
subrelstr (L,B,(x "\/" B)) is strict V58() reflexive transitive antisymmetric full meet-inheriting join-inheriting SubRelStr of L
x "/\" B is Element of the carrier of L
(L,(x "/\" B),x) is (L) Element of K32( the carrier of L)
subrelstr (L,(x "/\" B),x) is strict V58() reflexive transitive antisymmetric full meet-inheriting join-inheriting SubRelStr of L
the carrier of (subrelstr (L,B,(x "\/" B))) is set
the carrier of (subrelstr (L,(x "/\" B),x)) is set
y is set
a is Element of the carrier of L
x "/\" a is Element of the carrier of L
b is Element of the carrier of L
x "/\" (x "\/" B) is Element of the carrier of L
c is Element of the carrier of L
f1 is Element of the carrier of L
c "/\" x is Element of the carrier of L
K33( the carrier of (subrelstr (L,B,(x "\/" B))), the carrier of (subrelstr (L,(x "/\" B),x))) is set
K32(K33( the carrier of (subrelstr (L,B,(x "\/" B))), the carrier of (subrelstr (L,(x "/\" B),x)))) is non empty set
y is V7() V10( the carrier of (subrelstr (L,B,(x "\/" B)))) V11( the carrier of (subrelstr (L,(x "/\" B),x))) Function-like V21( the carrier of (subrelstr (L,B,(x "\/" B))), the carrier of (subrelstr (L,(x "/\" B),x))) Element of K32(K33( the carrier of (subrelstr (L,B,(x "\/" B))), the carrier of (subrelstr (L,(x "/\" B),x))))
a is V7() V10( the carrier of (subrelstr (L,B,(x "\/" B)))) V11( the carrier of (subrelstr (L,(x "/\" B),x))) Function-like V21( the carrier of (subrelstr (L,B,(x "\/" B))), the carrier of (subrelstr (L,(x "/\" B),x))) Element of K32(K33( the carrier of (subrelstr (L,B,(x "\/" B))), the carrier of (subrelstr (L,(x "/\" B),x))))
B "\/" x is Element of the carrier of L
(L,B,(B "\/" x)) is (L) Element of K32( the carrier of L)
subrelstr (L,B,(B "\/" x)) is strict V58() reflexive transitive antisymmetric full meet-inheriting join-inheriting SubRelStr of L
b is non empty V58() reflexive transitive antisymmetric with_suprema with_infima full meet-inheriting join-inheriting SubRelStr of L
the carrier of b is non empty set
c is non empty V58() reflexive transitive antisymmetric with_suprema with_infima full meet-inheriting join-inheriting SubRelStr of L
the carrier of c is non empty set
K33( the carrier of b, the carrier of c) is non empty set
K32(K33( the carrier of b, the carrier of c)) is non empty set
f1 is V7() V10( the carrier of b) V11( the carrier of c) Function-like V21( the carrier of b, the carrier of c) Element of K32(K33( the carrier of b, the carrier of c))
dom f1 is Element of K32( the carrier of b)
K32( the carrier of b) is non empty set
rng f1 is Element of K32( the carrier of c)
K32( the carrier of c) is non empty set
x1 is set
x2 is Element of the carrier of L
(x "/\" B) "\/" B is Element of the carrier of L
x2 "\/" B is Element of the carrier of L
f1 . (x2 "\/" B) is set
X2 is Element of the carrier of L
(x2 "\/" B) "/\" x is Element of the carrier of L
B "/\" x is Element of the carrier of L
x2 "\/" (B "/\" x) is Element of the carrier of L
x1 is Element of the carrier of b
x2 is Element of the carrier of b
f1 . x1 is Element of the carrier of c
f1 . x2 is Element of the carrier of c
X1 is Element of the carrier of L
f1 . X1 is set
X2 is Element of the carrier of L
f1 . X2 is set
[x1,x2] is Element of K33( the carrier of b, the carrier of b)
K33( the carrier of b, the carrier of b) is non empty set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
the InternalRel of b is V7() V10( the carrier of b) V11( the carrier of b) V20( the carrier of b) V87() V90() V94() Element of K32(K33( the carrier of b, the carrier of b))
K32(K33( the carrier of b, the carrier of b)) is non empty set
the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) V20( the carrier of L) V87() V90() V94() Element of K32(K33( the carrier of L, the carrier of L))
K33( the carrier of L, the carrier of L) is non empty set
K32(K33( the carrier of L, the carrier of L)) is non empty set
f1X1 is Element of the carrier of L
X1 "/\" x is Element of the carrier of L
f1X2 is Element of the carrier of L
X2 "/\" x is Element of the carrier of L
[(f1 . x1),(f1 . x2)] is Element of K33( the carrier of c, the carrier of c)
K33( the carrier of c, the carrier of c) is non empty set
{(f1 . x1),(f1 . x2)} is non empty set
{(f1 . x1)} is non empty set
{{(f1 . x1),(f1 . x2)},{(f1 . x1)}} is non empty set
the InternalRel of c is V7() V10( the carrier of c) V11( the carrier of c) V20( the carrier of c) V87() V90() V94() Element of K32(K33( the carrier of c, the carrier of c))
K32(K33( the carrier of c, the carrier of c)) is non empty set
the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) V20( the carrier of L) V87() V90() V94() Element of K32(K33( the carrier of L, the carrier of L))
K33( the carrier of L, the carrier of L) is non empty set
K32(K33( the carrier of L, the carrier of L)) is non empty set
f1X2 is Element of the carrier of L
f1X1 is Element of the carrier of L
X1 "/\" x is Element of the carrier of L
X2 "/\" x is Element of the carrier of L
x "/\" X2 is Element of the carrier of L
B "\/" (x "/\" X2) is Element of the carrier of L
x "/\" X1 is Element of the carrier of L
B "\/" (x "/\" X1) is Element of the carrier of L
(B "\/" x) "/\" X2 is Element of the carrier of L
(B "\/" x) "/\" X1 is Element of the carrier of L
x1 is set
K21(f1) is set
x2 is set
f1 . x1 is set
f1 . x2 is set
X2 is Element of the carrier of L
X1 is Element of the carrier of L
f1 . X1 is set
f1X1 is Element of the carrier of L
X1 "/\" x is Element of the carrier of L
f1 . X2 is set
f1X2 is Element of the carrier of L
X2 "/\" x is Element of the carrier of L
(B "\/" x) "/\" X1 is Element of the carrier of L
x "/\" X2 is Element of the carrier of L
B "\/" (x "/\" X2) is Element of the carrier of L
(B "\/" x) "/\" X2 is Element of the carrier of L
K33({{}},{{}}) is non empty set
K32(K33({{}},{{}})) is non empty set
the V7() V10({{}}) V11({{}}) V20({{}}) V87() V90() V94() Element of K32(K33({{}},{{}})) is V7() V10({{}}) V11({{}}) V20({{}}) V87() V90() V94() Element of K32(K33({{}},{{}}))
RelStr(# {{}}, the V7() V10({{}}) V11({{}}) V20({{}}) V87() V90() V94() Element of K32(K33({{}},{{}})) #) is non empty V48() finite 1 -element strict V58() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V161() RelStr
B is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
the Element of the carrier of L is Element of the carrier of L
B is Element of the carrier of L
x is set
B is set
{x} is non empty set
B \/ {x} is non empty set
a is Element of the carrier of L
y is Element of the carrier of L
a "/\" y is Element of the carrier of L
b is Element of the carrier of L
c 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
K32( the carrier of L) is non empty set
x is Element of K32( the carrier of L)