:: ROBBINS1 semantic presentation

K92() is V11() V24() V25() V26() V31() cardinal limit_cardinal set

K19(K92()) is V31() set

1 is V24() V25() V26() V30() V31() cardinal M2(K92())

K20(1,1) is set

K19(K20(1,1)) is set

K20(K20(1,1),1) is set

K19(K20(K20(1,1),1)) is set

0 is V11() V12() V24() V25() V26() V28() V29() V30() V31() cardinal 0 -element set

{0} is V11() V12() 1 -element set

op2 is V1() V4(K20(1,1)) V5(1) V6() V18(K20(1,1),1) M2(K19(K20(K20(1,1),1)))

op1 is V1() V4(1) V5(1) V6() V18(1,1) M2(K19(K20(1,1)))

(1,op2,op1) is () ()

() is () ()

(1,op2,op2,op1) is () ()

() is () ()

the carrier of () is set

the carrier of () is set

L is non empty V45() V46() 1 -element ()

the carrier of L is V11() V12() V31() 1 -element set

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

( the carrier of L, the of L) is () ()

the carrier of ( the carrier of L, the of L) is set

the carrier of () is V11() V12() V31() 1 -element set

the of () is V1() V4( the carrier of ()) V5( the carrier of ()) V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K19(K20( the carrier of (), the carrier of ())) is set

( the carrier of (), the of ()) is non empty V45() V46() 1 -element () ()

L is non empty ()

the carrier of L is V11() set

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

L9 is M2( the carrier of L)

the of L . L9 is M2( the carrier of L)

L is non empty ()

the carrier of L is V11() set

L is non empty ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,L9) "\/" (L,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,x)) is M2( the carrier of L)

the carrier of () is V11() V12() V31() 1 -element set

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

x "\/" L9 is M2( the carrier of ())

the L_join of () . (x,L9) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

y is M2( the carrier of ())

(L9 "\/" x) "\/" y is M2( the carrier of ())

the L_join of () . ((L9 "\/" x),y) is M2( the carrier of ())

x "\/" y is M2( the carrier of ())

the L_join of () . (x,y) is M2( the carrier of ())

L9 "\/" (x "\/" y) is M2( the carrier of ())

the L_join of () . (L9,(x "\/" y)) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

((),(L9 "\/" x)) is M2( the carrier of ())

the of () is V1() V4( the carrier of ()) V5( the carrier of ()) V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))

K19(K20( the carrier of (), the carrier of ())) is set

the of () . (L9 "\/" x) is M2( the carrier of ())

((),x) is M2( the carrier of ())

the of () . x is M2( the carrier of ())

L9 "\/" ((),x) is M2( the carrier of ())

the L_join of () . (L9,((),x)) is M2( the carrier of ())

((),(L9 "\/" ((),x))) is M2( the carrier of ())

the of () . (L9 "\/" ((),x)) is M2( the carrier of ())

((),(L9 "\/" x)) "\/" ((),(L9 "\/" ((),x))) is M2( the carrier of ())

the L_join of () . (((),(L9 "\/" x)),((),(L9 "\/" ((),x)))) is M2( the carrier of ())

((),(((),(L9 "\/" x)) "\/" ((),(L9 "\/" ((),x))))) is M2( the carrier of ())

the of () . (((),(L9 "\/" x)) "\/" ((),(L9 "\/" ((),x)))) is M2( the carrier of ())

L9 is M2( the carrier of ())

((),L9) is M2( the carrier of ())

the of () is V1() V4( the carrier of ()) V5( the carrier of ()) V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K19(K20( the carrier of (), the carrier of ())) is set

the of () . L9 is M2( the carrier of ())

x is M2( the carrier of ())

((),x) is M2( the carrier of ())

the of () . x is M2( the carrier of ())

((),L9) "\/" ((),x) is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (((),L9),((),x)) is M2( the carrier of ())

((),(((),L9) "\/" ((),x))) is M2( the carrier of ())

the of () . (((),L9) "\/" ((),x)) is M2( the carrier of ())

((),L9) "\/" x is M2( the carrier of ())

the L_join of () . (((),L9),x) is M2( the carrier of ())

((),(((),L9) "\/" x)) is M2( the carrier of ())

the of () . (((),L9) "\/" x) is M2( the carrier of ())

((),(((),L9) "\/" ((),x))) "\/" ((),(((),L9) "\/" x)) is M2( the carrier of ())

the L_join of () . (((),(((),L9) "\/" ((),x))),((),(((),L9) "\/" x))) is M2( the carrier of ())

L9 is M2( the carrier of ())

L9 "\/" L9 is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,L9) is M2( the carrier of ())

the carrier of () is V11() V12() V31() 1 -element set

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

x "\/" L9 is M2( the carrier of ())

the L_join of () . (x,L9) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

y is M2( the carrier of ())

(L9 "\/" x) "\/" y is M2( the carrier of ())

the L_join of () . ((L9 "\/" x),y) is M2( the carrier of ())

x "\/" y is M2( the carrier of ())

the L_join of () . (x,y) is M2( the carrier of ())

L9 "\/" (x "\/" y) is M2( the carrier of ())

the L_join of () . (L9,(x "\/" y)) is M2( the carrier of ())

L9 is M2( the carrier of ())

((),L9) is M2( the carrier of ())

the of () is V1() V4( the carrier of ()) V5( the carrier of ()) V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K19(K20( the carrier of (), the carrier of ())) is set

the of () . L9 is M2( the carrier of ())

x is M2( the carrier of ())

((),x) is M2( the carrier of ())

the of () . x is M2( the carrier of ())

((),L9) "\/" ((),x) is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (((),L9),((),x)) is M2( the carrier of ())

((),(((),L9) "\/" ((),x))) is M2( the carrier of ())

the of () . (((),L9) "\/" ((),x)) is M2( the carrier of ())

((),L9) "\/" x is M2( the carrier of ())

the L_join of () . (((),L9),x) is M2( the carrier of ())

((),(((),L9) "\/" x)) is M2( the carrier of ())

the of () . (((),L9) "\/" x) is M2( the carrier of ())

((),(((),L9) "\/" ((),x))) "\/" ((),(((),L9) "\/" x)) is M2( the carrier of ())

the L_join of () . (((),(((),L9) "\/" ((),x))),((),(((),L9) "\/" x))) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

((),(L9 "\/" x)) is M2( the carrier of ())

the of () is V1() V4( the carrier of ()) V5( the carrier of ()) V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))

K19(K20( the carrier of (), the carrier of ())) is set

the of () . (L9 "\/" x) is M2( the carrier of ())

((),x) is M2( the carrier of ())

the of () . x is M2( the carrier of ())

L9 "\/" ((),x) is M2( the carrier of ())

the L_join of () . (L9,((),x)) is M2( the carrier of ())

((),(L9 "\/" ((),x))) is M2( the carrier of ())

the of () . (L9 "\/" ((),x)) is M2( the carrier of ())

((),(L9 "\/" x)) "\/" ((),(L9 "\/" ((),x))) is M2( the carrier of ())

the L_join of () . (((),(L9 "\/" x)),((),(L9 "\/" ((),x)))) is M2( the carrier of ())

((),(((),(L9 "\/" x)) "\/" ((),(L9 "\/" ((),x))))) is M2( the carrier of ())

the of () . (((),(L9 "\/" x)) "\/" ((),(L9 "\/" ((),x)))) is M2( the carrier of ())

the carrier of () is V11() V12() V31() 1 -element set

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "/\" x is M2( the carrier of ())

the L_meet of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_meet of () . (L9,x) is M2( the carrier of ())

x "/\" L9 is M2( the carrier of ())

the L_meet of () . (x,L9) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "/\" x is M2( the carrier of ())

the L_meet of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_meet of () . (L9,x) is M2( the carrier of ())

y is M2( the carrier of ())

(L9 "/\" x) "/\" y is M2( the carrier of ())

the L_meet of () . ((L9 "/\" x),y) is M2( the carrier of ())

x "/\" y is M2( the carrier of ())

the L_meet of () . (x,y) is M2( the carrier of ())

L9 "/\" (x "/\" y) is M2( the carrier of ())

the L_meet of () . (L9,(x "/\" y)) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "/\" x is M2( the carrier of ())

the L_meet of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_meet of () . (L9,x) is M2( the carrier of ())

(L9 "/\" x) "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) commutative associative M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

the L_join of () . ((L9 "/\" x),x) is M2( the carrier of ())

L9 is M2( the carrier of ())

x is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

the L_join of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) commutative associative M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

K20( the carrier of (), the carrier of ()) is set

K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set

K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set

the L_join of () . (L9,x) is M2( the carrier of ())

L9 "/\" (L9 "\/" x) is M2( the carrier of ())

the L_meet of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))

the L_meet of () . (L9,(L9 "\/" x)) is M2( the carrier of ())

L9 "\/" x is M2( the carrier of ())

L9 "/\" (L9 "\/" x) is M2( the carrier of ())

the L_meet of () . (L9,(L9 "\/" x)) is M2( the carrier of ())

L is non empty join-commutative ()

the carrier of L is V11() set

y is M2( the carrier of L)

c is M2( the carrier of L)

y "\/" c is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (y,c) is M2( the carrier of L)

c "\/" y is M2( the carrier of L)

the L_join of L . (c,y) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,L9) "\/" (L,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,x)) is M2( the carrier of L)

(L,L9,(L,x)) is M2( the carrier of L)

(L,(L,x)) is M2( the carrier of L)

the of L . (L,x) is M2( the carrier of L)

(L,L9) "\/" (L,(L,x)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,x))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(L,x)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(L,x))) is M2( the carrier of L)

(L,(L,L9,x),(L,L9,(L,x))) is M2( the carrier of L)

the L_join of L . ((L,L9,x),(L,L9,(L,x))) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,L9,(L,L9)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,(L,L9)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,L9),(L,(L,L9))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,L9))) is M2( the carrier of L)

the of L . (L,(L,L9)) is M2( the carrier of L)

(L,(L,L9),(L,(L,(L,L9)))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,(L,L9)))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,(L,L9))))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,(L,L9)))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,L9)))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))) is M2( the carrier of L)

(L,(L,(L,L9)),(L,(L,(L,L9)))) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,(L,(L,L9)))) is M2( the carrier of L)

(L,(L,(L,(L,L9)),(L,(L,(L,L9))))) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),(L,(L,(L,L9)))) is M2( the carrier of L)

(L,(L,(L,L9)),(L,(L,L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,(L,L9)),(L,(L,L9)))) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,L9))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,L9))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,L9))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,L9))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9)))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,(L,L9)))),(L,(L,(L,L9),(L,(L,L9))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,(L,L9)))),(L,(L,(L,L9),(L,(L,L9))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,L9)),(L,(L,L9)))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,L9),(L,(L,(L,L9)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,L9)),(L,(L,L9)))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,L9),(L,(L,(L,L9)))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,(L,L9)),(L,(L,L9)))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,L9),(L,(L,(L,L9)))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,(L,L9)),(L,(L,L9)))),(L,(L,(L,L9),(L,(L,L9))))),(L,(L,(L,L9),(L,(L,(L,L9)))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9)))))) is M2( the carrier of L)

(L,(L,(L,L9)),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,L9)),(L,L9))) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,L9))),(L,(L,(L,(L,L9)),(L,(L,L9))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,L9))),(L,(L,(L,(L,L9)),(L,(L,L9))))) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9)))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,L9)),(L,L9))),(L,(L,(L,(L,L9)),(L,(L,L9))))),(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9))))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,L9)),(L,L9))),(L,(L,(L,(L,L9)),(L,(L,L9))))),(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9))))))) is M2( the carrier of L)

(L,(L,L9),(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9))))))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,(L,L9)),(L,(L,(L,L9))))))) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,(L,L9))) is M2( the carrier of L)

the of L . (L,(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,L9))),(L,(L,L9))) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,(L,(L,L9))),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9))),(L,(L,L9)))) is M2( the carrier of L)

the of L . (L,(L,(L,(L,L9))),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,(L,L9))),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9))),(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9))),(L,L9))) is M2( the carrier of L)

the of L . (L,(L,(L,(L,L9))),(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,L9))),(L,(L,L9)))),(L,(L,(L,(L,(L,L9))),(L,L9)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,L9))),(L,(L,L9)))),(L,(L,(L,(L,(L,L9))),(L,L9)))) is M2( the carrier of L)

(L,(L,L9),(L,(L,(L,L9)))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,(L,L9)))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,(L,L9))))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,(L,L9)))) is M2( the carrier of L)

(L,(L,L9),(L,(L,L9))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,L9)))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,L9))) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,(L,(L,L9))))),(L,(L,(L,L9),(L,(L,L9))))) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,L9,(L,L9)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,(L,L9)) is M2( the carrier of L)

x is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,x,(L,x)) is M2( the carrier of L)

the L_join of L . (x,(L,x)) is M2( the carrier of L)

(L,(L,x)) is M2( the carrier of L)

the of L . (L,x) is M2( the carrier of L)

(L,(L,L9),(L,(L,x))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,x))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,x)))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,x))) is M2( the carrier of L)

(L,(L,L9),(L,x)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,L9),(L,x))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))),(L,L9)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,(L,L9)),(L,(L,x))) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,(L,x))) is M2( the carrier of L)

(L,(L,(L,(L,L9)),(L,(L,x)))) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),(L,(L,x))) is M2( the carrier of L)

(L,(L,(L,L9)),(L,x)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,x)) is M2( the carrier of L)

(L,(L,(L,(L,L9)),(L,x))) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),(L,x)) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,x)))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))),(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))),(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,x))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,L9),(L,x)))))) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x))))) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,x))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,x))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x)))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,(L,L9),(L,x))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x))))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,(L,L9),(L,x))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x))))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,L9),(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,L9),(L,x)))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,L9),(L,x)))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,L9)),(L,x))),(L,(L,(L,L9),(L,x)))),(L,(L,(L,(L,L9),(L,(L,x)))),(L,(L,(L,(L,L9)),(L,(L,x)))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,L9),(L,(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,L9),(L,(L,x))))) is M2( the carrier of L)

(L,x,(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,L9),(L,(L,x)))))) is M2( the carrier of L)

the L_join of L . (x,(L,(L,(L,(L,(L,L9)),(L,(L,x)))),(L,(L,(L,L9),(L,(L,x)))))) is M2( the carrier of L)

L is non empty join-commutative join-associative () () ()

the carrier of L is V11() set

the M2( the carrier of L) is M2( the carrier of L)

(L, the M2( the carrier of L)) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . the M2( the carrier of L) is M2( the carrier of L)

(L,(L, the M2( the carrier of L)), the M2( the carrier of L)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L, the M2( the carrier of L)), the M2( the carrier of L)) is M2( the carrier of L)

x is M2( the carrier of L)

y is M2( the carrier of L)

(L,x,y) is M2( the carrier of L)

the L_join of L . (x,y) is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L . y is M2( the carrier of L)

(L,y,(L,y)) is M2( the carrier of L)

the L_join of L . (y,(L,y)) is M2( the carrier of L)

(L,(L,y),y) is M2( the carrier of L)

the L_join of L . ((L,y),y) is M2( the carrier of L)

(L,(L,(L,y),y),y) is M2( the carrier of L)

the L_join of L . ((L,(L,y),y),y) is M2( the carrier of L)

(L,y,y) is M2( the carrier of L)

the L_join of L . (y,y) is M2( the carrier of L)

(L,(L,y),(L,y,y)) is M2( the carrier of L)

the L_join of L . ((L,y),(L,y,y)) is M2( the carrier of L)

L is non empty join-commutative join-associative () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,x,L9) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (x,L9) is M2( the carrier of L)

y is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . y is M2( the carrier of L)

(L,y,(L,y)) is M2( the carrier of L)

the L_join of L . (y,(L,y)) is M2( the carrier of L)

L is non empty ()

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

Top L is M2( the carrier of L)

L9 is M2( the carrier of L)

the M2( the carrier of L) is M2( the carrier of L)

y is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . y is M2( the carrier of L)

(L,y,(L,y)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (y,(L,y)) is M2( the carrier of L)

c is M2( the carrier of L)

(L,(L,y,(L,y)),c) is M2( the carrier of L)

the L_join of L . ((L,y,(L,y)),c) is M2( the carrier of L)

(L,c,(L,y,(L,y))) is M2( the carrier of L)

the L_join of L . (c,(L,y,(L,y))) is M2( the carrier of L)

(L,c) is M2( the carrier of L)

the of L . c is M2( the carrier of L)

(L,c,(L,c)) is M2( the carrier of L)

the L_join of L . (c,(L,c)) is M2( the carrier of L)

(L,(L,c,(L,c)),c) is M2( the carrier of L)

the L_join of L . ((L,c,(L,c)),c) is M2( the carrier of L)

(L,c,c) is M2( the carrier of L)

the L_join of L . (c,c) is M2( the carrier of L)

(L,(L,c),(L,c,c)) is M2( the carrier of L)

the L_join of L . ((L,c),(L,c,c)) is M2( the carrier of L)

(L,(L,c),c) is M2( the carrier of L)

the L_join of L . ((L,c),c) is M2( the carrier of L)

(L,(L,y),y) is M2( the carrier of L)

the L_join of L . ((L,y),y) is M2( the carrier of L)

x is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,x,(L,x)) is M2( the carrier of L)

the L_join of L . (x,(L,x)) is M2( the carrier of L)

y is M2( the carrier of L)

(L,(L,x,(L,x)),y) is M2( the carrier of L)

the L_join of L . ((L,x,(L,x)),y) is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L . y is M2( the carrier of L)

(L,y,(L,y)) is M2( the carrier of L)

the L_join of L . (y,(L,y)) is M2( the carrier of L)

(L,(L,y,(L,y)),y) is M2( the carrier of L)

the L_join of L . ((L,y,(L,y)),y) is M2( the carrier of L)

(L,y,y) is M2( the carrier of L)

the L_join of L . (y,y) is M2( the carrier of L)

(L,(L,y),(L,y,y)) is M2( the carrier of L)

the L_join of L . ((L,y),(L,y,y)) is M2( the carrier of L)

(L,(L,y),y) is M2( the carrier of L)

the L_join of L . ((L,y),y) is M2( the carrier of L)

(L,(L,x),x) is M2( the carrier of L)

the L_join of L . ((L,x),x) is M2( the carrier of L)

y is M2( the carrier of L)

(L,y,(L,x,(L,x))) is M2( the carrier of L)

the L_join of L . (y,(L,x,(L,x))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

the M2( the carrier of L) is M2( the carrier of L)

(L, the M2( the carrier of L)) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . the M2( the carrier of L) is M2( the carrier of L)

(L,(L, the M2( the carrier of L)), the M2( the carrier of L)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L, the M2( the carrier of L)), the M2( the carrier of L)) is M2( the carrier of L)

(L,(L,(L, the M2( the carrier of L)), the M2( the carrier of L))) is M2( the carrier of L)

the of L . (L,(L, the M2( the carrier of L)), the M2( the carrier of L)) is M2( the carrier of L)

x is M2( the carrier of L)

y is M2( the carrier of L)

(L,x,y) is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L . y is M2( the carrier of L)

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

the L_join of L . ((L,x),(L,y)) is M2( the carrier of L)

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

the of L . ((L,x) "\/" (L,y)) is M2( the carrier of L)

(L,y,(L,y)) is M2( the carrier of L)

the L_join of L . (y,(L,y)) is M2( the carrier of L)

(L,(L,y,(L,y))) is M2( the carrier of L)

the of L . (L,y,(L,y)) is M2( the carrier of L)

(L,(L,(L, the M2( the carrier of L)), the M2( the carrier of L)),(L,y)) is M2( the carrier of L)

the L_join of L . ((L,(L, the M2( the carrier of L)), the M2( the carrier of L)),(L,y)) is M2( the carrier of L)

(L,(L,(L,(L, the M2( the carrier of L)), the M2( the carrier of L)),(L,y))) is M2( the carrier of L)

the of L . (L,(L,(L, the M2( the carrier of L)), the M2( the carrier of L)),(L,y)) is M2( the carrier of L)

(L,(L,y),y) is M2( the carrier of L)

the L_join of L . ((L,y),y) is M2( the carrier of L)

(L,(L,(L,y),y),(L,y)) is M2( the carrier of L)

the L_join of L . ((L,(L,y),y),(L,y)) is M2( the carrier of L)

(L,(L,(L,(L,y),y),(L,y))) is M2( the carrier of L)

the of L . (L,(L,(L,y),y),(L,y)) is M2( the carrier of L)

(L,(L,y),(L,y)) is M2( the carrier of L)

the L_join of L . ((L,y),(L,y)) is M2( the carrier of L)

(L,y,(L,(L,y),(L,y))) is M2( the carrier of L)

the L_join of L . (y,(L,(L,y),(L,y))) is M2( the carrier of L)

(L,(L,y,(L,(L,y),(L,y)))) is M2( the carrier of L)

the of L . (L,y,(L,(L,y),(L,y))) is M2( the carrier of L)

L is non empty join-commutative join-associative ()

the carrier of L is V11() set

y is M2( the carrier of L)

c is M2( the carrier of L)

(L,y,c) is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . y is M2( the carrier of L)

(L,c) is M2( the carrier of L)

the of L . c is M2( the carrier of L)

(L,y) "\/" (L,c) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,y),(L,c)) is M2( the carrier of L)

(L,((L,y) "\/" (L,c))) is M2( the carrier of L)

the of L . ((L,y) "\/" (L,c)) is M2( the carrier of L)

(L,c,y) is M2( the carrier of L)

(L,c) "\/" (L,y) is M2( the carrier of L)

the L_join of L . ((L,c),(L,y)) is M2( the carrier of L)

(L,((L,c) "\/" (L,y))) is M2( the carrier of L)

the of L . ((L,c) "\/" (L,y)) is M2( the carrier of L)

(L,(L,y),(L,c)) is M2( the carrier of L)

(L,(L,(L,y),(L,c))) is M2( the carrier of L)

the of L . (L,(L,y),(L,c)) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,x,L9) is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . x is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L . L9 is M2( the carrier of L)

(L,x) "\/" (L,L9) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,x),(L,L9)) is M2( the carrier of L)

(L,((L,x) "\/" (L,L9))) is M2( the carrier of L)

the of L . ((L,x) "\/" (L,L9)) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

(L) is M2( the carrier of L)

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,L9,(L,L9)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,(L,L9)) is M2( the carrier of L)

(L,(L,L9,(L,L9))) is M2( the carrier of L)

the of L . (L,L9,(L,L9)) is M2( the carrier of L)

x is M2( the carrier of L)

(L,(L,(L,L9,(L,L9))),x) is M2( the carrier of L)

(L,(L,(L,L9,(L,L9)))) is M2( the carrier of L)

the of L . (L,(L,L9,(L,L9))) is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,(L,(L,L9,(L,L9)))) "\/" (L,x) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9,(L,L9)))),(L,x)) is M2( the carrier of L)

(L,((L,(L,(L,L9,(L,L9)))) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,(L,(L,L9,(L,L9)))) "\/" (L,x)) is M2( the carrier of L)

(L,x,(L,x)) is M2( the carrier of L)

the L_join of L . (x,(L,x)) is M2( the carrier of L)

(L,(L,x,(L,x))) is M2( the carrier of L)

the of L . (L,x,(L,x)) is M2( the carrier of L)

(L,(L,(L,x,(L,x)))) is M2( the carrier of L)

the of L . (L,(L,x,(L,x))) is M2( the carrier of L)

(L,(L,(L,(L,x,(L,x)))),(L,x)) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,x,(L,x)))),(L,x)) is M2( the carrier of L)

(L,(L,(L,(L,(L,x,(L,x)))),(L,x))) is M2( the carrier of L)

the of L . (L,(L,(L,(L,x,(L,x)))),(L,x)) is M2( the carrier of L)

(L,(L,x,(L,x)),(L,x)) is M2( the carrier of L)

the L_join of L . ((L,x,(L,x)),(L,x)) is M2( the carrier of L)

(L,(L,(L,x,(L,x)),(L,x))) is M2( the carrier of L)

the of L . (L,(L,x,(L,x)),(L,x)) is M2( the carrier of L)

(L,(L,x),(L,x)) is M2( the carrier of L)

the L_join of L . ((L,x),(L,x)) is M2( the carrier of L)

(L,x,(L,(L,x),(L,x))) is M2( the carrier of L)

the L_join of L . (x,(L,(L,x),(L,x))) is M2( the carrier of L)

(L,(L,x,(L,(L,x),(L,x)))) is M2( the carrier of L)

the of L . (L,x,(L,(L,x),(L,x))) is M2( the carrier of L)

(L,(L,L9),L9) is M2( the carrier of L)

the L_join of L . ((L,L9),L9) is M2( the carrier of L)

(L,(L,(L,L9),L9)) is M2( the carrier of L)

the of L . (L,(L,L9),L9) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

Top L is M2( the carrier of L)

the carrier of L is V11() set

(L,(Top L)) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . (Top L) is M2( the carrier of L)

(L) is M2( the carrier of L)

(L,(L)) is M2( the carrier of L)

the of L . (L) is M2( the carrier of L)

the M2( the carrier of L) is M2( the carrier of L)

(L, the M2( the carrier of L)) is M2( the carrier of L)

the of L . the M2( the carrier of L) is M2( the carrier of L)

(L, the M2( the carrier of L),(L, the M2( the carrier of L))) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ( the M2( the carrier of L),(L, the M2( the carrier of L))) is M2( the carrier of L)

(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L)))) is M2( the carrier of L)

the of L . (L, the M2( the carrier of L),(L, the M2( the carrier of L))) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . x is M2( the carrier of L)

(L,x,(L,x)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (x,(L,x)) is M2( the carrier of L)

(L,(L,x,(L,x))) is M2( the carrier of L)

the of L . (L,x,(L,x)) is M2( the carrier of L)

(L,L9,(L,(L,x,(L,x)))) is M2( the carrier of L)

the L_join of L . (L9,(L,(L,x,(L,x)))) is M2( the carrier of L)

(L,(L,(L,x,(L,x)))) is M2( the carrier of L)

the of L . (L,(L,x,(L,x))) is M2( the carrier of L)

(L,(L,(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x))))) is M2( the carrier of L)

(L,(L,(L,(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x)))))) is M2( the carrier of L)

the of L . (L,(L,(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x))))) is M2( the carrier of L)

(L,(L,(L,(L,x,(L,x)))),(L,(L,x,(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,x,(L,x)))),(L,(L,x,(L,x)))) is M2( the carrier of L)

(L,(L,(L,(L,(L,x,(L,x)))),(L,(L,x,(L,x))))) is M2( the carrier of L)

the of L . (L,(L,(L,(L,x,(L,x)))),(L,(L,x,(L,x)))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x)))))),(L,(L,(L,(L,(L,x,(L,x)))),(L,(L,x,(L,x)))))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x)))))),(L,(L,(L,(L,(L,x,(L,x)))),(L,(L,x,(L,x)))))) is M2( the carrier of L)

(L,(L,x,(L,x)),(L,x,(L,x))) is M2( the carrier of L)

the L_join of L . ((L,x,(L,x)),(L,x,(L,x))) is M2( the carrier of L)

(L,(L,(L,x,(L,x)),(L,x,(L,x)))) is M2( the carrier of L)

the of L . (L,(L,x,(L,x)),(L,x,(L,x))) is M2( the carrier of L)

(L,(L,(L,(L,x,(L,x)),(L,x,(L,x)))),(L,(L,x,(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,x,(L,x)),(L,x,(L,x)))),(L,(L,x,(L,x)))) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L . L9 is M2( the carrier of L)

(L,(L,L9),L9) is M2( the carrier of L)

the L_join of L . ((L,L9),L9) is M2( the carrier of L)

(L,(L,x,(L,x)),(L,(L,x,(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,x,(L,x)),(L,(L,x,(L,x)))) is M2( the carrier of L)

(L,(L,(L,x,(L,x)),(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x)),(L,x,(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,x,(L,x)),(L,(L,x,(L,x)))),(L,(L,(L,x,(L,x)),(L,x,(L,x))))) is M2( the carrier of L)

(L,(L,x,(L,x)),(L,(L,(L,x,(L,x)),(L,x,(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,x,(L,x)),(L,(L,(L,x,(L,x)),(L,x,(L,x))))) is M2( the carrier of L)

(L,(L,(L,x,(L,x)),(L,x,(L,x))),(L,(L,(L,x,(L,x)),(L,x,(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,(L,x,(L,x)),(L,x,(L,x))),(L,(L,(L,x,(L,x)),(L,x,(L,x))))) is M2( the carrier of L)

(L,(L,L9),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,L9)) is M2( the carrier of L)

(L,(L,(L,L9),(L,L9))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,L9)) is M2( the carrier of L)

(L,(L,(L,L9),L9)) is M2( the carrier of L)

the of L . (L,(L,L9),L9) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,L9))),(L,(L,(L,L9),L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,L9))),(L,(L,(L,L9),L9))) is M2( the carrier of L)

(L,(L,(L,(L,L9),L9)),(L,(L,(L,L9),L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),L9)),(L,(L,(L,L9),L9))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9),(L,L9))),(L,(L,(L,L9),L9))),(L,(L,(L,(L,L9),L9)),(L,(L,(L,L9),L9)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9),(L,L9))),(L,(L,(L,L9),L9))),(L,(L,(L,(L,L9),L9)),(L,(L,(L,L9),L9)))) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,L9))),(L,(L,(L,(L,L9),L9)),(L,(L,(L,L9),L9)))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,L9))),(L,(L,(L,(L,L9),L9)),(L,(L,(L,L9),L9)))) is M2( the carrier of L)

L is non empty join-commutative join-associative () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9,L9) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,L9) is M2( the carrier of L)

(L,(L,L9,L9)) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . (L,L9,L9) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L . L9 is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,(L,L9)),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,L9)),(L,L9))) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),(L,L9)) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,L9))),(L,(L,L9,L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,L9))),(L,(L,L9,L9))) is M2( the carrier of L)

(L,(L,(L,L9)),L9) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),L9) is M2( the carrier of L)

(L,(L,(L,(L,L9)),L9)) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),L9) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9)),(L,L9))),(L,(L,(L,(L,L9)),L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9)),(L,L9))),(L,(L,(L,(L,L9)),L9))) is M2( the carrier of L)

(L,(L,(L,L9,L9))) is M2( the carrier of L)

the of L . (L,(L,L9,L9)) is M2( the carrier of L)

L is non empty ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

L9 "\/" L9 is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,L9) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

(L) is M2( the carrier of L)

L9 is M2( the carrier of L)

(L,L9,(L)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,(L)) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,(L,L9),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,L9)) is M2( the carrier of L)

(L,(L,(L,L9),(L,L9))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,L9)) is M2( the carrier of L)

(L,(L,L9),L9) is M2( the carrier of L)

the L_join of L . ((L,L9),L9) is M2( the carrier of L)

(L,(L,(L,L9),L9)) is M2( the carrier of L)

the of L . (L,(L,L9),L9) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,L9))),(L,(L,(L,L9),L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,L9))),(L,(L,(L,L9),L9))) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,(L,L9)),(L,(L,(L,L9),L9))) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,(L,(L,L9),L9))) is M2( the carrier of L)

(L,L9,(L,(L,(L,L9),L9))) is M2( the carrier of L)

the L_join of L . (L9,(L,(L,(L,L9),L9))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

Top L is M2( the carrier of L)

L9 is M2( the carrier of L)

(L,L9,(Top L)) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,(Top L)) is M2( the carrier of L)

the of L . (Top L) is M2( the carrier of L)

(L,L9) "\/" (L,(Top L)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,(Top L))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(Top L)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(Top L))) is M2( the carrier of L)

(L) is M2( the carrier of L)

(L,(L,L9),(L)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L)) is M2( the carrier of L)

(L,(L,(L,L9),(L))) is M2( the carrier of L)

the of L . (L,(L,L9),(L)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

(L) is M2( the carrier of L)

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,L9,(L,L9)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,L9) "\/" (L,(L,L9)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,(L,L9))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(L,L9)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(L,L9))) is M2( the carrier of L)

Top L is M2( the carrier of L)

(L,(Top L)) is M2( the carrier of L)

the of L . (Top L) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

y is M2( the carrier of L)

(L,x,y) is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . x is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L . y is M2( the carrier of L)

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

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,x),(L,y)) is M2( the carrier of L)

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

the of L . ((L,x) "\/" (L,y)) is M2( the carrier of L)

(L,L9,(L,x,y)) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L . L9 is M2( the carrier of L)

(L,(L,x,y)) is M2( the carrier of L)

the of L . (L,x,y) is M2( the carrier of L)

(L,L9) "\/" (L,(L,x,y)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,x,y))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(L,x,y)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(L,x,y))) is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

(L,L9) "\/" (L,x) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,x)) is M2( the carrier of L)

(L,(L,L9,x),y) is M2( the carrier of L)

(L,(L,L9,x)) is M2( the carrier of L)

the of L . (L,L9,x) is M2( the carrier of L)

(L,(L,L9,x)) "\/" (L,y) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,x)),(L,y)) is M2( the carrier of L)

(L,((L,(L,L9,x)) "\/" (L,y))) is M2( the carrier of L)

the of L . ((L,(L,L9,x)) "\/" (L,y)) is M2( the carrier of L)

(L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,L9),(L,x)),(L,y)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9),(L,x)),(L,y)) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,x)),(L,y))) is M2( the carrier of L)

the of L . (L,(L,(L,L9),(L,x)),(L,y)) is M2( the carrier of L)

(L,(L,x),(L,y)) is M2( the carrier of L)

(L,(L,L9),(L,(L,x),(L,y))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,x),(L,y))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,x),(L,y)))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,x),(L,y))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,x) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,x)) is M2( the carrier of L)

the of L . (L,x) is M2( the carrier of L)

(L,(L,L9)) "\/" (L,(L,x)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,(L,x))) is M2( the carrier of L)

(L,((L,(L,L9)) "\/" (L,(L,x)))) is M2( the carrier of L)

the of L . ((L,(L,L9)) "\/" (L,(L,x))) is M2( the carrier of L)

(L,(L,(L,L9),(L,x))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,L9)),x) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),x) is M2( the carrier of L)

(L,(L,(L,(L,L9)),x)) is M2( the carrier of L)

the of L . (L,(L,(L,L9)),x) is M2( the carrier of L)

(L,(L,L9,x)) is M2( the carrier of L)

the of L . (L,L9,x) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

(L,L9,L9) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,L9) "\/" (L,L9) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,L9)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,L9))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,L9)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

Top L is M2( the carrier of L)

L9 is M2( the carrier of L)

(L,L9,(Top L)) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,(Top L)) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,L9,(L,L9)) is M2( the carrier of L)

the L_join of L . (L9,(L,L9)) is M2( the carrier of L)

(L,L9,(L,L9,(L,L9))) is M2( the carrier of L)

the L_join of L . (L9,(L,L9,(L,L9))) is M2( the carrier of L)

(L,L9,L9) is M2( the carrier of L)

the L_join of L . (L9,L9) is M2( the carrier of L)

(L,(L,L9,L9),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,L9,L9),(L,L9)) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,L9) "\/" (L,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,x)) is M2( the carrier of L)

(L,L9,(L,L9,x)) is M2( the carrier of L)

the L_join of L . (L9,(L,L9,x)) is M2( the carrier of L)

(L,L9,(L,x)) is M2( the carrier of L)

(L,(L,x)) is M2( the carrier of L)

the of L . (L,x) is M2( the carrier of L)

(L,L9) "\/" (L,(L,x)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,x))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(L,x)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(L,x))) is M2( the carrier of L)

(L,(L,L9,x),(L,L9,(L,x))) is M2( the carrier of L)

the L_join of L . ((L,L9,x),(L,L9,(L,x))) is M2( the carrier of L)

(L,(L,L9,x),(L,(L,L9,x),(L,L9,(L,x)))) is M2( the carrier of L)

the L_join of L . ((L,L9,x),(L,(L,L9,x),(L,L9,(L,x)))) is M2( the carrier of L)

(L,(L,L9,x),(L,L9,x)) is M2( the carrier of L)

the L_join of L . ((L,L9,x),(L,L9,x)) is M2( the carrier of L)

(L,(L,(L,L9,x),(L,L9,x)),(L,L9,(L,x))) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,x),(L,L9,x)),(L,L9,(L,x))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,x) is M2( the carrier of L)

(L,L9,(L,L9,x)) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,(L,L9,x)) is M2( the carrier of L)

the of L . (L,L9,x) is M2( the carrier of L)

(L,L9) "\/" (L,(L,L9,x)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,L9,x))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(L,L9,x)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(L,L9,x))) is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,x)) is M2( the carrier of L)

the of L . (L,x) is M2( the carrier of L)

(L,(L,L9)) "\/" (L,(L,x)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,(L,x))) is M2( the carrier of L)

(L,((L,(L,L9)) "\/" (L,(L,x)))) is M2( the carrier of L)

the of L . ((L,(L,L9)) "\/" (L,(L,x))) is M2( the carrier of L)

(L,(L,(L,L9),(L,x))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,x)))) is M2( the carrier of L)

the of L . (L,(L,(L,L9),(L,x))) is M2( the carrier of L)

(L,(L,L9),(L,(L,(L,(L,L9),(L,x))))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,(L,(L,L9),(L,x))))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,(L,(L,L9),(L,x)))))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,(L,(L,L9),(L,x))))) is M2( the carrier of L)

(L,(L,L9),(L,(L,L9),(L,x))) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,L9),(L,x))) is M2( the carrier of L)

(L,(L,(L,L9),(L,(L,L9),(L,x)))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,(L,L9),(L,x))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

Top L is M2( the carrier of L)

L9 is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,(L,L9),x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),x) is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,(L,x),L9) is M2( the carrier of L)

the L_join of L . ((L,x),L9) is M2( the carrier of L)

(L,(L,L9),(L,x)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,L9),(L,x))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,L9),x)) is M2( the carrier of L)

the of L . (L,(L,L9),x) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,x))),(L,(L,(L,L9),x))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),(L,x))),(L,(L,(L,L9),x))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

Top L is M2( the carrier of L)

(L) is M2( the carrier of L)

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . (L9,x) is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,L9) "\/" (L,x) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,x)) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,(L,L9)),x) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),x) is M2( the carrier of L)

(L,(L,x),(L,L9)) is M2( the carrier of L)

the L_join of L . ((L,x),(L,L9)) is M2( the carrier of L)

(L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,L9),(L,x))) is M2( the carrier of L)

the of L . (L,(L,L9),(L,x)) is M2( the carrier of L)

(L,(L,(L,(L,L9),(L,x)))) is M2( the carrier of L)

the of L . (L,(L,(L,L9),(L,x))) is M2( the carrier of L)

L is non empty join-commutative join-associative upper-bounded () () ()

the carrier of L is V11() set

Top L is M2( the carrier of L)

L9 is M2( the carrier of L)

x is M2( the carrier of L)

(L,L9,x) is M2( the carrier of L)

(L,L9) is M2( the carrier of L)

the of L is V1() V4( the carrier of L) V5( the carrier of L) V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))

K20( the carrier of L, the carrier of L) is set

K19(K20( the carrier of L, the carrier of L)) is set

the of L . L9 is M2( the carrier of L)

(L,x) is M2( the carrier of L)

the of L . x is M2( the carrier of L)

(L,L9) "\/" (L,x) is M2( the carrier of L)

the L_join of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))

K20(K20( the carrier of L, the carrier of L), the carrier of L) is set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

the L_join of L . ((L,L9),(L,x)) is M2( the carrier of L)

(L,((L,L9) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,x)) is M2( the carrier of L)

y is M2( the carrier of L)

(L,(L,L9,x),y) is M2( the carrier of L)

(L,(L,L9,x)) is M2( the carrier of L)

the of L . (L,L9,x) is M2( the carrier of L)

(L,y) is M2( the carrier of L)

the of L . y is M2( the carrier of L)

(L,(L,L9,x)) "\/" (L,y) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,x)),(L,y)) is M2( the carrier of L)

(L,((L,(L,L9,x)) "\/" (L,y))) is M2( the carrier of L)

the of L . ((L,(L,L9,x)) "\/" (L,y)) is M2( the carrier of L)

(L,(L,L9,x),(L,y)) is M2( the carrier of L)

(L,(L,y)) is M2( the carrier of L)

the of L . (L,y) is M2( the carrier of L)

(L,(L,L9,x)) "\/" (L,(L,y)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,x)),(L,(L,y))) is M2( the carrier of L)

(L,((L,(L,L9,x)) "\/" (L,(L,y)))) is M2( the carrier of L)

the of L . ((L,(L,L9,x)) "\/" (L,(L,y))) is M2( the carrier of L)

(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,x),y),(L,(L,L9,x),(L,y))) is M2( the carrier of L)

(L,L9,(L,x)) is M2( the carrier of L)

(L,(L,x)) is M2( the carrier of L)

the of L . (L,x) is M2( the carrier of L)

(L,L9) "\/" (L,(L,x)) is M2( the carrier of L)

the L_join of L . ((L,L9),(L,(L,x))) is M2( the carrier of L)

(L,((L,L9) "\/" (L,(L,x)))) is M2( the carrier of L)

the of L . ((L,L9) "\/" (L,(L,x))) is M2( the carrier of L)

(L,(L,L9,(L,x)),y) is M2( the carrier of L)

(L,(L,L9,(L,x))) is M2( the carrier of L)

the of L . (L,L9,(L,x)) is M2( the carrier of L)

(L,(L,L9,(L,x))) "\/" (L,y) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,(L,x))),(L,y)) is M2( the carrier of L)

(L,((L,(L,L9,(L,x))) "\/" (L,y))) is M2( the carrier of L)

the of L . ((L,(L,L9,(L,x))) "\/" (L,y)) is M2( the carrier of L)

(L,(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)) is M2( the carrier of L)

(L,(L,L9,(L,x)),(L,y)) is M2( the carrier of L)

(L,(L,L9,(L,x))) "\/" (L,(L,y)) is M2( the carrier of L)

the L_join of L . ((L,(L,L9,(L,x))),(L,(L,y))) is M2( the carrier of L)

(L,((L,(L,L9,(L,x))) "\/" (L,(L,y)))) is M2( the carrier of L)

the of L . ((L,(L,L9,(L,x))) "\/" (L,(L,y))) is M2( the carrier of L)

(L,(L,(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)),(L,(L,L9,(L,x)),(L,y))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)),(L,(L,L9,(L,x)),(L,y))) is M2( the carrier of L)

(L,(L,L9),x) is M2( the carrier of L)

(L,(L,L9)) is M2( the carrier of L)

the of L . (L,L9) is M2( the carrier of L)

(L,(L,L9)) "\/" (L,x) is M2( the carrier of L)

the L_join of L . ((L,(L,L9)),(L,x)) is M2( the carrier of L)

(L,((L,(L,L9)) "\/" (L,x))) is M2( the carrier of L)

the of L . ((L,(L,L9)) "\/" (L,x)) is M2( the carrier of L)

(L,(L,(L,L9),x),y) is M2( the carrier of L)

(L,(L,(L,L9),x)) is M2( the carrier of L)

the of L . (L,(L,L9),x) is M2( the carrier of L)

(L,(L,(L,L9),x)) "\/" (L,y) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),x)),(L,y)) is M2( the carrier of L)

(L,((L,(L,(L,L9),x)) "\/" (L,y))) is M2( the carrier of L)

the of L . ((L,(L,(L,L9),x)) "\/" (L,y)) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)),(L,(L,L9,(L,x)),(L,y))),(L,(L,(L,L9),x),y)) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)),(L,(L,L9,(L,x)),(L,y))),(L,(L,(L,L9),x),y)) is M2( the carrier of L)

(L,(L,(L,L9),x),(L,y)) is M2( the carrier of L)

(L,(L,(L,L9),x)) "\/" (L,(L,y)) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,L9),x)),(L,(L,y))) is M2( the carrier of L)

(L,((L,(L,(L,L9),x)) "\/" (L,(L,y)))) is M2( the carrier of L)

the of L . ((L,(L,(L,L9),x)) "\/" (L,(L,y))) is M2( the carrier of L)

(L,(L,(L,(L,(L,(L,(L,L9,x),y),(L,(L,L9,x),(L,y))),(L,(L,L9,(L,x)),y)),(L,(L,L9,(L,x)),(L,y))),(L,(L,(L,L9),x),y)),(L,(L,(L,L9),x),(L,y))) is M2( the carrier of L)

the L_join of L . ((L,(L,(L,(L,(L,(L,L9,x),y),(L,(L,L9,x),