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