let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun d,q is u.t.i.
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun d,q is u.t.i.
let d be BiFunction of A,L; :: thesis: ( d is symmetric & d is u.t.i. implies for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun d,q is u.t.i. )
assume that
A1: d is symmetric and
A2: d is u.t.i. ; :: thesis: for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun d,q is u.t.i.
reconsider B = {{A},{{A}},{{{A}}}} as non empty set ;
let q be Element of [:A,A,the carrier of L,the carrier of L:]; :: thesis: ( d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) implies new_bi_fun d,q is u.t.i. )
set x = q `1 ;
set y = q `2 ;
set f = new_bi_fun d,q;
reconsider a = q `3 , b = q `4 as Element of L ;
A3: for p, q, u being Element of new_set A st p in A & q in B & u in A holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in A & q in B & u in A implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume A4: ( p in A & q in B & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

per cases ( ( p in A & u in A & q = {A} ) or ( p in A & u in A & q = {{A}} ) or ( p in A & u in A & q = {{{A}}} ) ) by A4, ENUMSET1:def 1;

suppose A5: ( p in A & u in A & q = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then reconsider p9 = p, u9 = u as Element of A ;
d . p9,u9 <= (d . p9,(q `1 )) "\/" (d . (q `1 ),u9) by A2, Def8;
then A6: ( (d . p9,(q `1 )) "\/" (d . u9,(q `1 )) <= ((d . p9,(q `1 )) "\/" (d . u9,(q `1 ))) "\/" a & d . p9,u9 <= (d . p9,(q `1 )) "\/" (d . u9,(q `1 )) ) by A1, Def6, YELLOW_0:22;
((d . p9,(q `1 )) "\/" (d . u9,(q `1 ))) "\/" a = (d . p9,(q `1 )) "\/" ((d . u9,(q `1 )) "\/" a) by LATTICE3:14
.= (d . p9,(q `1 )) "\/" ((d . u9,(q `1 )) "\/" (a "\/" a)) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" (((d . u9,(q `1 )) "\/" a) "\/" a) by LATTICE3:14
.= ((d . p9,(q `1 )) "\/" a) "\/" ((d . u9,(q `1 )) "\/" a) by LATTICE3:14 ;
then A7: d . p9,u9 <= ((d . p9,(q `1 )) "\/" a) "\/" ((d . u9,(q `1 )) "\/" a) by A6, ORDERS_2:26;
( (new_bi_fun d,q) . p,q = (d . p9,(q `1 )) "\/" a & (new_bi_fun d,q) . q,u = (d . u9,(q `1 )) "\/" a ) by A5, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A7, Def11; :: thesis: verum

end;

suppose A8: ( p in A & u in A & q = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then reconsider p9 = p, u9 = u as Element of A ;
d . p9,u9 <= (d . p9,(q `1 )) "\/" (d . (q `1 ),u9) by A2, Def8;
then A9: ( (d . p9,(q `1 )) "\/" (d . u9,(q `1 )) <= ((d . p9,(q `1 )) "\/" (d . u9,(q `1 ))) "\/" (a "\/" b) & d . p9,u9 <= (d . p9,(q `1 )) "\/" (d . u9,(q `1 )) ) by A1, Def6, YELLOW_0:22;
((d . p9,(q `1 )) "\/" (d . u9,(q `1 ))) "\/" (a "\/" b) = (d . p9,(q `1 )) "\/" ((d . u9,(q `1 )) "\/" (a "\/" b)) by LATTICE3:14
.= (d . p9,(q `1 )) "\/" ((d . u9,(q `1 )) "\/" ((a "\/" b) "\/" (a "\/" b))) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" (((d . u9,(q `1 )) "\/" (a "\/" b)) "\/" (a "\/" b)) by LATTICE3:14
.= ((d . p9,(q `1 )) "\/" (a "\/" b)) "\/" ((d . u9,(q `1 )) "\/" (a "\/" b)) by LATTICE3:14
.= (((d . p9,(q `1 )) "\/" a) "\/" b) "\/" ((d . u9,(q `1 )) "\/" (a "\/" b)) by LATTICE3:14
.= (((d . p9,(q `1 )) "\/" a) "\/" b) "\/" (((d . u9,(q `1 )) "\/" a) "\/" b) by LATTICE3:14 ;
then A10: d . p9,u9 <= (((d . p9,(q `1 )) "\/" a) "\/" b) "\/" (((d . u9,(q `1 )) "\/" a) "\/" b) by A9, ORDERS_2:26;
( (new_bi_fun d,q) . p,q = ((d . p9,(q `1 )) "\/" a) "\/" b & (new_bi_fun d,q) . q,u = ((d . u9,(q `1 )) "\/" a) "\/" b ) by A8, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A10, Def11; :: thesis: verum

end;

suppose A11: ( p in A & u in A & q = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then reconsider p9 = p, u9 = u as Element of A ;
d . p9,u9 <= (d . p9,(q `2 )) "\/" (d . (q `2 ),u9) by A2, Def8;
then A12: ( (d . p9,(q `2 )) "\/" (d . u9,(q `2 )) <= ((d . p9,(q `2 )) "\/" (d . u9,(q `2 ))) "\/" b & d . p9,u9 <= (d . p9,(q `2 )) "\/" (d . u9,(q `2 )) ) by A1, Def6, YELLOW_0:22;
((d . p9,(q `2 )) "\/" (d . u9,(q `2 ))) "\/" b = (d . p9,(q `2 )) "\/" ((d . u9,(q `2 )) "\/" b) by LATTICE3:14
.= (d . p9,(q `2 )) "\/" ((d . u9,(q `2 )) "\/" (b "\/" b)) by YELLOW_5:1
.= (d . p9,(q `2 )) "\/" (((d . u9,(q `2 )) "\/" b) "\/" b) by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" b) "\/" ((d . u9,(q `2 )) "\/" b) by LATTICE3:14 ;
then A13: d . p9,u9 <= ((d . p9,(q `2 )) "\/" b) "\/" ((d . u9,(q `2 )) "\/" b) by A12, ORDERS_2:26;
( (new_bi_fun d,q) . p,q = (d . p9,(q `2 )) "\/" b & (new_bi_fun d,q) . q,u = (d . u9,(q `2 )) "\/" b ) by A11, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A13, Def11; :: thesis: verum

end;

end;

end;

assume A14: d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) ; :: thesis: new_bi_fun d,q is u.t.i.
A15: for p, q, u being Element of new_set A st p in B & q in B & u in A holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in B & q in B & u in A implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume that
A16: ( p in B & q in B ) and
A17: u in A ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)
reconsider u9 = u as Element of A by A17;

per cases ( ( u in A & q = {A} & p = {A} ) or ( u in A & q = {A} & p = {{A}} ) or ( u in A & q = {A} & p = {{{A}}} ) or ( u in A & q = {{A}} & p = {A} ) or ( u in A & q = {{A}} & p = {{A}} ) or ( u in A & q = {{A}} & p = {{{A}}} ) or ( u in A & q = {{{A}}} & p = {A} ) or ( u in A & q = {{{A}}} & p = {{A}} ) or ( u in A & q = {{{A}}} & p = {{{A}}} ) ) by A16, A17, ENUMSET1:def 1;

suppose A18: ( u in A & q = {A} & p = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (new_bi_fun d,q) . p,u by A18, WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) ; :: thesis: verum

end;

suppose A19: ( u in A & q = {A} & p = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = b "\/" ((new_bi_fun d,q) . q,u) by Def11
.= ((d . u9,(q `1 )) "\/" a) "\/" b by A19, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A19, Def11; :: thesis: verum

end;

suppose A20: ( u in A & q = {A} & p = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

b "\/" (a "\/" b) = (b "\/" b) "\/" a by LATTICE3:14
.= b "\/" a by YELLOW_5:1
.= b "\/" (a "\/" a) by YELLOW_5:1
.= a "\/" (a "\/" b) by LATTICE3:14 ;
then A21: ((d . u9,(q `1 )) "\/" b) "\/" (a "\/" b) = (d . u9,(q `1 )) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= (a "\/" b) "\/" ((d . u9,(q `1 )) "\/" a) by LATTICE3:14
.= ((new_bi_fun d,q) . p,q) "\/" ((d . u9,(q `1 )) "\/" a) by A20, Def11 ;
d . u9,(q `2 ) <= (d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A2, Def8;
then A22: (d . u9,(q `2 )) "\/" b <= ((d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b by WAYBEL_1:3;
(d . u9,(q `1 )) "\/" b <= (d . u9,(q `1 )) "\/" b ;
then A23: ( ((d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b = ((d . u9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) & ((d . u9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) <= ((d . u9,(q `1 )) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
(new_bi_fun d,q) . p,u = (d . u9,(q `2 )) "\/" b by A20, Def11;
then (new_bi_fun d,q) . p,u <= ((d . u9,(q `1 )) "\/" b) "\/" (a "\/" b) by A22, A23, ORDERS_2:26;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A20, A21, Def11; :: thesis: verum

end;

suppose A24: ( u in A & q = {{A}} & p = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = b "\/" ((new_bi_fun d,q) . q,u) by Def11
.= b "\/" (((d . u9,(q `1 )) "\/" a) "\/" b) by A24, Def11
.= b "\/" (b "\/" ((new_bi_fun d,q) . p,u)) by A24, Def11
.= (b "\/" b) "\/" ((new_bi_fun d,q) . p,u) by LATTICE3:14
.= b "\/" ((new_bi_fun d,q) . p,u) by YELLOW_5:1 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:22; :: thesis: verum

end;

suppose A25: ( u in A & q = {{A}} & p = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (new_bi_fun d,q) . p,u by A25, WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) ; :: thesis: verum

end;

suppose A26: ( u in A & q = {{A}} & p = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

b "\/" (a "\/" b) = (b "\/" b) "\/" a by LATTICE3:14
.= b "\/" a by YELLOW_5:1
.= b "\/" (a "\/" a) by YELLOW_5:1
.= (a "\/" b) "\/" a by LATTICE3:14 ;
then A27: ((d . u9,(q `1 )) "\/" b) "\/" (a "\/" b) = (d . u9,(q `1 )) "\/" ((a "\/" b) "\/" a) by LATTICE3:14
.= ((d . u9,(q `1 )) "\/" (a "\/" b)) "\/" a by LATTICE3:14
.= (((d . u9,(q `1 )) "\/" a) "\/" b) "\/" a by LATTICE3:14
.= ((new_bi_fun d,q) . p,q) "\/" (((d . u9,(q `1 )) "\/" a) "\/" b) by A26, Def11 ;
(d . u9,(q `1 )) "\/" b <= (d . u9,(q `1 )) "\/" b ;
then A28: ( ((d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b = ((d . u9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) & ((d . u9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) <= ((d . u9,(q `1 )) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
d . u9,(q `2 ) <= (d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A2, Def8;
then A29: (d . u9,(q `2 )) "\/" b <= ((d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b by WAYBEL_1:3;
(new_bi_fun d,q) . p,u = (d . u9,(q `2 )) "\/" b by A26, Def11;
then (new_bi_fun d,q) . p,u <= ((d . u9,(q `1 )) "\/" b) "\/" (a "\/" b) by A29, A28, ORDERS_2:26;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A26, A27, Def11; :: thesis: verum

end;

suppose A30: ( u in A & q = {{{A}}} & p = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

A31: a "\/" (a "\/" b) = (a "\/" a) "\/" b by LATTICE3:14
.= a "\/" b by YELLOW_5:1
.= a "\/" (b "\/" b) by YELLOW_5:1
.= b "\/" (a "\/" b) by LATTICE3:14 ;
A32: (a "\/" (d . u9,(q `2 ))) "\/" (a "\/" b) = (d . u9,(q `2 )) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= ((d . u9,(q `2 )) "\/" b) "\/" (a "\/" b) by A31, LATTICE3:14
.= ((new_bi_fun d,q) . p,q) "\/" ((d . u9,(q `2 )) "\/" b) by A30, Def11 ;
a "\/" (d . u9,(q `2 )) <= a "\/" (d . u9,(q `2 )) ;
then A33: (a "\/" (d . u9,(q `2 ))) "\/" (d . (q `1 ),(q `2 )) <= (a "\/" (d . u9,(q `2 ))) "\/" (a "\/" b) by A14, YELLOW_3:3;
d . u9,(q `1 ) <= (d . u9,(q `2 )) "\/" (d . (q `2 ),(q `1 )) by A2, Def8;
then A34: (d . u9,(q `1 )) "\/" a <= ((d . u9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" a by WAYBEL_1:3;
A35: ((d . u9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" a = (d . (q `2 ),(q `1 )) "\/" ((d . u9,(q `2 )) "\/" a) by LATTICE3:14
.= (a "\/" (d . u9,(q `2 ))) "\/" (d . (q `1 ),(q `2 )) by A1, Def6 ;
(new_bi_fun d,q) . p,u = (d . u9,(q `1 )) "\/" a by A30, Def11;
then (new_bi_fun d,q) . p,u <= (a "\/" (d . u9,(q `2 ))) "\/" (a "\/" b) by A34, A35, A33, ORDERS_2:26;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A30, A32, Def11; :: thesis: verum

end;

suppose A36: ( u in A & q = {{{A}}} & p = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A37: (new_bi_fun d,q) . p,u = ((d . u9,(q `1 )) "\/" a) "\/" b by Def11
.= (d . u9,(q `1 )) "\/" (a "\/" b) by LATTICE3:14 ;
(a "\/" b) "\/" (d . u9,(q `2 )) <= (a "\/" b) "\/" (d . u9,(q `2 )) ;
then A38: ((a "\/" b) "\/" (d . u9,(q `2 ))) "\/" (d . (q `1 ),(q `2 )) <= ((a "\/" b) "\/" (d . u9,(q `2 ))) "\/" (a "\/" b) by A14, YELLOW_3:3;
d . u9,(q `1 ) <= (d . u9,(q `2 )) "\/" (d . (q `2 ),(q `1 )) by A2, Def8;
then A39: (d . u9,(q `1 )) "\/" (a "\/" b) <= ((d . u9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" (a "\/" b) by WAYBEL_1:3;
A40: ((d . u9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" (a "\/" b) = ((a "\/" b) "\/" (d . u9,(q `2 ))) "\/" (d . (q `2 ),(q `1 )) by LATTICE3:14
.= ((a "\/" b) "\/" (d . u9,(q `2 ))) "\/" (d . (q `1 ),(q `2 )) by A1, Def6 ;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = a "\/" ((new_bi_fun d,q) . q,u) by A36, Def11
.= a "\/" (b "\/" (d . u9,(q `2 ))) by A36, Def11
.= (a "\/" b) "\/" (d . u9,(q `2 )) by LATTICE3:14
.= ((a "\/" b) "\/" (a "\/" b)) "\/" (d . u9,(q `2 )) by YELLOW_5:1
.= (a "\/" b) "\/" ((d . u9,(q `2 )) "\/" (a "\/" b)) by LATTICE3:14 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A37, A39, A40, A38, ORDERS_2:26; :: thesis: verum

end;

suppose A41: ( u in A & q = {{{A}}} & p = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (new_bi_fun d,q) . p,u by A41, WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) ; :: thesis: verum

end;

end;

end;

A42: for p, q, u being Element of new_set A st p in B & q in A & u in A holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in B & q in A & u in A implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume that
A43: p in B and
A44: ( q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)
reconsider q9 = q, u9 = u as Element of A by A44;

per cases ( ( p = {A} & q in A & u in A ) or ( p = {{A}} & q in A & u in A ) or ( p = {{{A}}} & q in A & u in A ) ) by A43, A44, ENUMSET1:def 1;

suppose A45: ( p = {A} & q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . u9,(q `1 ) <= (d . u9,q9) "\/" (d . q9,(q `1 )) by A2, Def8;
then d . u9,(q `1 ) <= (d . q9,u9) "\/" (d . q9,(q `1 )) by A1, Def6;
then (d . u9,(q `1 )) "\/" a <= ((d . q9,(q `1 )) "\/" (d . q9,u9)) "\/" a by WAYBEL_1:3;
then A46: (d . u9,(q `1 )) "\/" a <= ((d . q9,(q `1 )) "\/" a) "\/" (d . q9,u9) by LATTICE3:14;
A47: (new_bi_fun d,q) . q,u = d . q9,u9 by Def11;
(new_bi_fun d,q) . p,q = (d . q9,(q `1 )) "\/" a by A45, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A45, A47, A46, Def11; :: thesis: verum

end;

suppose A48: ( p = {{A}} & q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . u9,(q `1 ) <= (d . u9,q9) "\/" (d . q9,(q `1 )) by A2, Def8;
then d . u9,(q `1 ) <= (d . q9,u9) "\/" (d . q9,(q `1 )) by A1, Def6;
then (d . u9,(q `1 )) "\/" (a "\/" b) <= ((d . q9,(q `1 )) "\/" (d . q9,u9)) "\/" (a "\/" b) by WAYBEL_1:3;
then ((d . u9,(q `1 )) "\/" a) "\/" b <= ((d . q9,(q `1 )) "\/" (d . q9,u9)) "\/" (a "\/" b) by LATTICE3:14;
then ((d . u9,(q `1 )) "\/" a) "\/" b <= ((d . q9,(q `1 )) "\/" (a "\/" b)) "\/" (d . q9,u9) by LATTICE3:14;
then A49: ((d . u9,(q `1 )) "\/" a) "\/" b <= (((d . q9,(q `1 )) "\/" a) "\/" b) "\/" (d . q9,u9) by LATTICE3:14;
A50: (new_bi_fun d,q) . q,u = d . q9,u9 by Def11;
(new_bi_fun d,q) . p,q = ((d . q9,(q `1 )) "\/" a) "\/" b by A48, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A48, A50, A49, Def11; :: thesis: verum

end;

suppose A51: ( p = {{{A}}} & q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . u9,(q `2 ) <= (d . u9,q9) "\/" (d . q9,(q `2 )) by A2, Def8;
then d . u9,(q `2 ) <= (d . q9,u9) "\/" (d . q9,(q `2 )) by A1, Def6;
then (d . u9,(q `2 )) "\/" b <= ((d . q9,(q `2 )) "\/" (d . q9,u9)) "\/" b by WAYBEL_1:3;
then A52: (d . u9,(q `2 )) "\/" b <= ((d . q9,(q `2 )) "\/" b) "\/" (d . q9,u9) by LATTICE3:14;
A53: (new_bi_fun d,q) . q,u = d . q9,u9 by Def11;
(new_bi_fun d,q) . p,q = (d . q9,(q `2 )) "\/" b by A51, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A51, A53, A52, Def11; :: thesis: verum

end;

end;

end;

A54: for p, q, u being Element of new_set A st p in A & q in A & u in B holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in A & q in A & u in B implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume A55: ( p in A & q in A & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

per cases ( ( p in A & q in A & u = {A} ) or ( p in A & q in A & u = {{A}} ) or ( p in A & q in A & u = {{{A}}} ) ) by A55, ENUMSET1:def 1;

suppose A56: ( p in A & q in A & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then reconsider p9 = p, q9 = q as Element of A ;
A57: (new_bi_fun d,q) . p,q = d . p9,q9 by Def11;
d . p9,(q `1 ) <= (d . p9,q9) "\/" (d . q9,(q `1 )) by A2, Def8;
then A58: (d . p9,(q `1 )) "\/" a <= ((d . p9,q9) "\/" (d . q9,(q `1 ))) "\/" a by WAYBEL_1:3;
( (new_bi_fun d,q) . p,u = (d . p9,(q `1 )) "\/" a & (new_bi_fun d,q) . q,u = (d . q9,(q `1 )) "\/" a ) by A56, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A57, A58, LATTICE3:14; :: thesis: verum

end;

suppose A59: ( p in A & q in A & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then reconsider p9 = p, q9 = q as Element of A ;
A60: (new_bi_fun d,q) . p,q = d . p9,q9 by Def11;
d . p9,(q `1 ) <= (d . p9,q9) "\/" (d . q9,(q `1 )) by A2, Def8;
then (d . p9,(q `1 )) "\/" a <= ((d . p9,q9) "\/" (d . q9,(q `1 ))) "\/" a by WAYBEL_1:3;
then ((d . p9,(q `1 )) "\/" a) "\/" b <= (((d . p9,q9) "\/" (d . q9,(q `1 ))) "\/" a) "\/" b by WAYBEL_1:3;
then A61: ((d . p9,(q `1 )) "\/" a) "\/" b <= ((d . p9,q9) "\/" ((d . q9,(q `1 )) "\/" a)) "\/" b by LATTICE3:14;
( (new_bi_fun d,q) . p,u = ((d . p9,(q `1 )) "\/" a) "\/" b & (new_bi_fun d,q) . q,u = ((d . q9,(q `1 )) "\/" a) "\/" b ) by A59, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A60, A61, LATTICE3:14; :: thesis: verum

end;

suppose A62: ( p in A & q in A & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then reconsider p9 = p, q9 = q as Element of A ;
A63: (new_bi_fun d,q) . p,q = d . p9,q9 by Def11;
d . p9,(q `2 ) <= (d . p9,q9) "\/" (d . q9,(q `2 )) by A2, Def8;
then A64: (d . p9,(q `2 )) "\/" b <= ((d . p9,q9) "\/" (d . q9,(q `2 ))) "\/" b by WAYBEL_1:3;
( (new_bi_fun d,q) . p,u = (d . p9,(q `2 )) "\/" b & (new_bi_fun d,q) . q,u = (d . q9,(q `2 )) "\/" b ) by A62, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A63, A64, LATTICE3:14; :: thesis: verum

end;

end;

end;

A65: for p, q, u being Element of new_set A st p in B & q in B & u in B holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in B & q in B & u in B implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume A66: ( p in B & q in B & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

per cases ( ( p = {A} & q = {A} & u = {A} ) or ( p = {A} & q = {A} & u = {{A}} ) or ( p = {A} & q = {A} & u = {{{A}}} ) or ( p = {A} & q = {{A}} & u = {A} ) or ( p = {A} & q = {{A}} & u = {{A}} ) or ( p = {A} & q = {{A}} & u = {{{A}}} ) or ( p = {A} & q = {{{A}}} & u = {A} ) or ( p = {A} & q = {{{A}}} & u = {{A}} ) or ( p = {A} & q = {{{A}}} & u = {{{A}}} ) or ( p = {{A}} & q = {A} & u = {A} ) or ( p = {{A}} & q = {A} & u = {{A}} ) or ( p = {{A}} & q = {A} & u = {{{A}}} ) or ( p = {{A}} & q = {{A}} & u = {A} ) or ( p = {{A}} & q = {{A}} & u = {{A}} ) or ( p = {{A}} & q = {{A}} & u = {{{A}}} ) or ( p = {{A}} & q = {{{A}}} & u = {A} ) or ( p = {{A}} & q = {{{A}}} & u = {{A}} ) or ( p = {{A}} & q = {{{A}}} & u = {{{A}}} ) or ( p = {{{A}}} & q = {A} & u = {A} ) or ( p = {{{A}}} & q = {A} & u = {{A}} ) or ( p = {{{A}}} & q = {A} & u = {{{A}}} ) or ( p = {{{A}}} & q = {{A}} & u = {A} ) or ( p = {{{A}}} & q = {{A}} & u = {{A}} ) or ( p = {{{A}}} & q = {{A}} & u = {{{A}}} ) or ( p = {{{A}}} & q = {{{A}}} & u = {A} ) or ( p = {{{A}}} & q = {{{A}}} & u = {{A}} ) or ( p = {{{A}}} & q = {{{A}}} & u = {{{A}}} ) ) by A66, ENUMSET1:def 1;

suppose A67: ( p = {A} & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A67, Def11; :: thesis: verum

end;

suppose A68: ( p = {A} & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,u) by Def11
.= (Bottom L) "\/" b by A68, Def11
.= b by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A68, Def11; :: thesis: verum

end;

suppose A69: ( p = {A} & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,u) by Def11
.= (Bottom L) "\/" (a "\/" b) by A69, Def11
.= a "\/" b by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A69, Def11; :: thesis: verum

end;

suppose A70: ( p = {A} & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A70, Def11; :: thesis: verum

end;

suppose A71: ( p = {A} & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = b "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (Bottom L) "\/" b by A71, Def11
.= b by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A71, Def11; :: thesis: verum

end;

suppose A72: ( p = {A} & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = b "\/" ((new_bi_fun d,q) . q,u) by Def11
.= a "\/" b by A72, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A72, Def11; :: thesis: verum

end;

suppose A73: ( p = {A} & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A73, Def11; :: thesis: verum

end;

suppose A74: ( p = {A} & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A75: (new_bi_fun d,q) . p,u = b by Def11;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (a "\/" b) "\/" ((new_bi_fun d,q) . q,u) by A74, Def11
.= (b "\/" a) "\/" a by A74, Def11
.= b "\/" (a "\/" a) by LATTICE3:14
.= b "\/" a by YELLOW_5:1 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A75, YELLOW_0:22; :: thesis: verum

end;

suppose A76: ( p = {A} & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (a "\/" b) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (Bottom L) "\/" (a "\/" b) by A76, Def11
.= a "\/" b by WAYBEL_1:4
.= (new_bi_fun d,q) . p,q by A76, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A76; :: thesis: verum

end;

suppose A77: ( p = {{A}} & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = b "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (Bottom L) "\/" b by A77, Def11
.= b by WAYBEL_1:4
.= (new_bi_fun d,q) . p,q by A77, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A77; :: thesis: verum

end;

suppose A78: ( p = {{A}} & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A78, Def11; :: thesis: verum

end;

suppose A79: ( p = {{A}} & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A80: (new_bi_fun d,q) . p,u = a by Def11;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = b "\/" ((new_bi_fun d,q) . q,u) by A79, Def11
.= b "\/" (b "\/" a) by A79, Def11
.= (b "\/" b) "\/" a by LATTICE3:14
.= b "\/" a by YELLOW_5:1 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A80, YELLOW_0:22; :: thesis: verum

end;

suppose A81: ( p = {{A}} & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,u) by Def11
.= (Bottom L) "\/" b by A81, Def11
.= b by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A81, Def11; :: thesis: verum

end;

suppose A82: ( p = {{A}} & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A82, Def11; :: thesis: verum

end;

suppose A83: ( p = {{A}} & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,u) by Def11
.= (Bottom L) "\/" a by A83, Def11
.= a by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A83, Def11; :: thesis: verum

end;

suppose A84: ( p = {{A}} & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A85: (new_bi_fun d,q) . p,u = b by Def11;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = a "\/" ((new_bi_fun d,q) . q,u) by A84, Def11
.= a "\/" (a "\/" b) by A84, Def11
.= (a "\/" a) "\/" b by LATTICE3:14
.= a "\/" b by YELLOW_5:1 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A85, YELLOW_0:22; :: thesis: verum

end;

suppose A86: ( p = {{A}} & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A86, Def11; :: thesis: verum

end;

suppose A87: ( p = {{A}} & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = a "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (Bottom L) "\/" a by A87, Def11
.= a by WAYBEL_1:4
.= (new_bi_fun d,q) . p,q by A87, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A87; :: thesis: verum

end;

suppose A88: ( p = {{{A}}} & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (a "\/" b) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (Bottom L) "\/" (a "\/" b) by A88, Def11
.= a "\/" b by WAYBEL_1:4
.= (new_bi_fun d,q) . p,q by A88, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A88; :: thesis: verum

end;

suppose A89: ( p = {{{A}}} & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A90: (new_bi_fun d,q) . p,u = a by Def11;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (a "\/" b) "\/" ((new_bi_fun d,q) . q,u) by A89, Def11
.= (a "\/" b) "\/" b by A89, Def11
.= a "\/" (b "\/" b) by LATTICE3:14
.= a "\/" b by YELLOW_5:1 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A90, YELLOW_0:22; :: thesis: verum

end;

suppose A91: ( p = {{{A}}} & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A91, Def11; :: thesis: verum

end;

suppose A92: ( p = {{{A}}} & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = a "\/" ((new_bi_fun d,q) . q,u) by Def11
.= a "\/" b by A92, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A92, Def11; :: thesis: verum

end;

suppose A93: ( p = {{{A}}} & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = a "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (Bottom L) "\/" a by A93, Def11
.= a by WAYBEL_1:4
.= (new_bi_fun d,q) . p,q by A93, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A93; :: thesis: verum

end;

suppose A94: ( p = {{{A}}} & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A94, Def11; :: thesis: verum

end;

suppose A95: ( p = {{{A}}} & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,u) by Def11
.= (Bottom L) "\/" (a "\/" b) by A95, Def11
.= a "\/" b by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A95, Def11; :: thesis: verum

end;

suppose A96: ( p = {{{A}}} & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,u) by Def11
.= (Bottom L) "\/" a by A96, Def11
.= a by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A96, Def11; :: thesis: verum

end;

suppose A97: ( p = {{{A}}} & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

Bottom L <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A97, Def11; :: thesis: verum

end;

end;

end;

A98: for p, q, u being Element of new_set A st p in B & q in A & u in B holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in B & q in A & u in B implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume that
A99: p in B and
A100: q in A and
A101: u in B ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)
reconsider q9 = q as Element of A by A100;

per cases ( ( q in A & p = {A} & u = {A} ) or ( q in A & p = {A} & u = {{A}} ) or ( q in A & p = {A} & u = {{{A}}} ) or ( q in A & p = {{A}} & u = {A} ) or ( q in A & p = {{A}} & u = {{A}} ) or ( q in A & p = {{A}} & u = {{{A}}} ) or ( q in A & p = {{{A}}} & u = {A} ) or ( q in A & p = {{{A}}} & u = {{A}} ) or ( q in A & p = {{{A}}} & u = {{{A}}} ) ) by A99, A100, A101, ENUMSET1:def 1;

suppose ( q in A & p = {A} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then (new_bi_fun d,q) . p,u = Bottom L by Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44; :: thesis: verum

end;

suppose A102: ( q in A & p = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A103: ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = ((new_bi_fun d,q) . p,q) "\/" (((d . q9,(q `1 )) "\/" a) "\/" b) by Def11
.= ((new_bi_fun d,q) . p,q) "\/" ((d . q9,(q `1 )) "\/" (a "\/" b)) by LATTICE3:14
.= (((new_bi_fun d,q) . p,q) "\/" (d . q9,(q `1 ))) "\/" (a "\/" b) by LATTICE3:14
.= ((((new_bi_fun d,q) . p,q) "\/" (d . q9,(q `1 ))) "\/" a) "\/" b by LATTICE3:14 ;
(new_bi_fun d,q) . p,u = b by A102, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A103, YELLOW_0:22; :: thesis: verum

end;

suppose A104: ( q in A & p = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A105: (new_bi_fun d,q) . p,u = a "\/" b by Def11;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = ((d . q9,(q `1 )) "\/" a) "\/" ((new_bi_fun d,q) . q,u) by A104, Def11
.= ((d . q9,(q `1 )) "\/" a) "\/" ((d . q9,(q `2 )) "\/" b) by A104, Def11
.= (d . q9,(q `1 )) "\/" (a "\/" ((d . q9,(q `2 )) "\/" b)) by LATTICE3:14
.= (d . q9,(q `1 )) "\/" ((d . q9,(q `2 )) "\/" (a "\/" b)) by LATTICE3:14
.= ((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" (a "\/" b) by LATTICE3:14 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A105, YELLOW_0:22; :: thesis: verum

end;

suppose A106: ( q in A & p = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A107: ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (((d . q9,(q `1 )) "\/" a) "\/" b) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= ((new_bi_fun d,q) . q,u) "\/" ((d . q9,(q `1 )) "\/" (a "\/" b)) by LATTICE3:14
.= (((new_bi_fun d,q) . q,u) "\/" (d . q9,(q `1 ))) "\/" (a "\/" b) by LATTICE3:14
.= ((((new_bi_fun d,q) . q,u) "\/" (d . q9,(q `1 ))) "\/" a) "\/" b by LATTICE3:14 ;
(new_bi_fun d,q) . p,u = b by A106, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A107, YELLOW_0:22; :: thesis: verum

end;

suppose ( q in A & p = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then (new_bi_fun d,q) . p,u = Bottom L by Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44; :: thesis: verum

end;

suppose A108: ( q in A & p = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A109: ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (((d . q9,(q `1 )) "\/" a) "\/" b) "\/" ((new_bi_fun d,q) . q,u) by Def11
.= (a "\/" ((d . q9,(q `1 )) "\/" b)) "\/" ((new_bi_fun d,q) . q,u) by LATTICE3:14
.= a "\/" (((d . q9,(q `1 )) "\/" b) "\/" ((new_bi_fun d,q) . q,u)) by LATTICE3:14 ;
(new_bi_fun d,q) . p,u = a by A108, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A109, YELLOW_0:22; :: thesis: verum

end;

suppose A110: ( q in A & p = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A111: (new_bi_fun d,q) . p,u = a "\/" b by Def11;
((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = ((d . q9,(q `2 )) "\/" b) "\/" ((new_bi_fun d,q) . q,u) by A110, Def11
.= ((d . q9,(q `2 )) "\/" b) "\/" ((d . q9,(q `1 )) "\/" a) by A110, Def11
.= (d . q9,(q `2 )) "\/" (b "\/" ((d . q9,(q `1 )) "\/" a)) by LATTICE3:14
.= (d . q9,(q `2 )) "\/" ((d . q9,(q `1 )) "\/" (b "\/" a)) by LATTICE3:14
.= ((d . q9,(q `2 )) "\/" (d . q9,(q `1 ))) "\/" (a "\/" b) by LATTICE3:14 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A111, YELLOW_0:22; :: thesis: verum

end;

suppose A112: ( q in A & p = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then A113: ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = ((new_bi_fun d,q) . p,q) "\/" (((d . q9,(q `1 )) "\/" a) "\/" b) by Def11
.= ((new_bi_fun d,q) . p,q) "\/" ((d . q9,(q `1 )) "\/" (a "\/" b)) by LATTICE3:14
.= (((new_bi_fun d,q) . p,q) "\/" (d . q9,(q `1 ))) "\/" (a "\/" b) by LATTICE3:14
.= ((((new_bi_fun d,q) . p,q) "\/" (d . q9,(q `1 ))) "\/" b) "\/" a by LATTICE3:14 ;
(new_bi_fun d,q) . p,u = a by A112, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A113, YELLOW_0:22; :: thesis: verum

end;

suppose ( q in A & p = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then (new_bi_fun d,q) . p,u = Bottom L by Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:44; :: thesis: verum

end;

end;

end;

A114: for p, q, u being Element of new_set A st p in A & q in B & u in B holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in A & q in B & u in B implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume that
A115: p in A and
A116: ( q in B & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)
reconsider p9 = p as Element of A by A115;

per cases ( ( p in A & q = {A} & u = {A} ) or ( p in A & q = {A} & u = {{A}} ) or ( p in A & q = {A} & u = {{{A}}} ) or ( p in A & q = {{A}} & u = {A} ) or ( p in A & q = {{A}} & u = {{A}} ) or ( p in A & q = {{A}} & u = {{{A}}} ) or ( p in A & q = {{{A}}} & u = {A} ) or ( p in A & q = {{{A}}} & u = {{A}} ) or ( p in A & q = {{{A}}} & u = {{{A}}} ) ) by A115, A116, ENUMSET1:def 1;

suppose A117: ( p in A & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,q) by Def11
.= (new_bi_fun d,q) . p,q by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A117; :: thesis: verum

end;

suppose A118: ( p in A & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then (new_bi_fun d,q) . p,u = ((d . p9,(q `1 )) "\/" a) "\/" b by Def11
.= ((new_bi_fun d,q) . p,q) "\/" b by A118, Def11 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A118, Def11; :: thesis: verum

end;

suppose A119: ( p in A & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . p9,(q `2 ) <= (d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A2, Def8;
then (d . p9,(q `2 )) "\/" b <= ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b by WAYBEL_1:3;
then A120: (new_bi_fun d,q) . p,u <= ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b by A119, Def11;
(d . p9,(q `1 )) "\/" b <= (d . p9,(q `1 )) "\/" b ;
then ( ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b = ((d . p9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) & ((d . p9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) <= ((d . p9,(q `1 )) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
then A121: (new_bi_fun d,q) . p,u <= ((d . p9,(q `1 )) "\/" b) "\/" (a "\/" b) by A120, ORDERS_2:26;
A122: ((d . p9,(q `1 )) "\/" b) "\/" (a "\/" b) = (d . p9,(q `1 )) "\/" ((b "\/" a) "\/" b) by LATTICE3:14
.= (d . p9,(q `1 )) "\/" (a "\/" (b "\/" b)) by LATTICE3:14
.= (d . p9,(q `1 )) "\/" (a "\/" b) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" ((a "\/" a) "\/" b) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= ((d . p9,(q `1 )) "\/" a) "\/" (a "\/" b) by LATTICE3:14 ;
(new_bi_fun d,q) . p,q = (d . p9,(q `1 )) "\/" a by A119, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A119, A121, A122, Def11; :: thesis: verum

end;

suppose A123: ( p in A & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then (new_bi_fun d,q) . p,q = ((d . p9,(q `1 )) "\/" a) "\/" b by Def11
.= ((new_bi_fun d,q) . p,u) "\/" b by A123, Def11 ;
then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (((new_bi_fun d,q) . p,u) "\/" b) "\/" b by A123, Def11
.= ((new_bi_fun d,q) . p,u) "\/" (b "\/" b) by LATTICE3:14
.= ((new_bi_fun d,q) . p,u) "\/" b by YELLOW_5:1 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by YELLOW_0:22; :: thesis: verum

end;

suppose A124: ( p in A & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,q) by Def11
.= (new_bi_fun d,q) . p,q by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A124; :: thesis: verum

end;

suppose A125: ( p in A & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . p9,(q `2 ) <= (d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A2, Def8;
then (d . p9,(q `2 )) "\/" b <= ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b by WAYBEL_1:3;
then A126: (new_bi_fun d,q) . p,u <= ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b by A125, Def11;
(d . p9,(q `1 )) "\/" b <= (d . p9,(q `1 )) "\/" b ;
then ( ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" b = ((d . p9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) & ((d . p9,(q `1 )) "\/" b) "\/" (d . (q `1 ),(q `2 )) <= ((d . p9,(q `1 )) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
then A127: (new_bi_fun d,q) . p,u <= ((d . p9,(q `1 )) "\/" b) "\/" (a "\/" b) by A126, ORDERS_2:26;
A128: ((d . p9,(q `1 )) "\/" b) "\/" (a "\/" b) = (d . p9,(q `1 )) "\/" ((b "\/" a) "\/" b) by LATTICE3:14
.= (d . p9,(q `1 )) "\/" (a "\/" (b "\/" b)) by LATTICE3:14
.= (d . p9,(q `1 )) "\/" (a "\/" b) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" ((a "\/" a) "\/" b) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= ((d . p9,(q `1 )) "\/" (a "\/" b)) "\/" a by LATTICE3:14
.= (((d . p9,(q `1 )) "\/" a) "\/" b) "\/" a by LATTICE3:14 ;
(new_bi_fun d,q) . p,q = ((d . p9,(q `1 )) "\/" a) "\/" b by A125, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A125, A127, A128, Def11; :: thesis: verum

end;

suppose A129: ( p in A & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . p9,(q `1 ) <= (d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 )) by A2, Def8;
then (d . p9,(q `1 )) "\/" a <= ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" a by WAYBEL_1:3;
then A130: (new_bi_fun d,q) . p,u <= ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" a by A129, Def11;
( d . (q `2 ),(q `1 ) <= a "\/" b & (d . p9,(q `2 )) "\/" a <= (d . p9,(q `2 )) "\/" a ) by A1, A14, Def6;
then ( ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" a = ((d . p9,(q `2 )) "\/" a) "\/" (d . (q `2 ),(q `1 )) & ((d . p9,(q `2 )) "\/" a) "\/" (d . (q `2 ),(q `1 )) <= ((d . p9,(q `2 )) "\/" a) "\/" (a "\/" b) ) by LATTICE3:14, YELLOW_3:3;
then A131: (new_bi_fun d,q) . p,u <= ((d . p9,(q `2 )) "\/" a) "\/" (a "\/" b) by A130, ORDERS_2:26;
A132: ((d . p9,(q `2 )) "\/" a) "\/" (a "\/" b) = (((d . p9,(q `2 )) "\/" a) "\/" a) "\/" b by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" (a "\/" a)) "\/" b by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" a) "\/" b by YELLOW_5:1
.= (d . p9,(q `2 )) "\/" (a "\/" b) by LATTICE3:14
.= (d . p9,(q `2 )) "\/" (a "\/" (b "\/" b)) by YELLOW_5:1
.= (d . p9,(q `2 )) "\/" ((a "\/" b) "\/" b) by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" b) "\/" (a "\/" b) by LATTICE3:14 ;
(new_bi_fun d,q) . p,q = (d . p9,(q `2 )) "\/" b by A129, Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A129, A131, A132, Def11; :: thesis: verum

end;

suppose A133: ( p in A & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

d . p9,(q `1 ) <= (d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 )) by A2, Def8;
then A134: (d . p9,(q `1 )) "\/" (a "\/" b) <= ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" (a "\/" b) by WAYBEL_1:3;
(new_bi_fun d,q) . p,u = ((d . p9,(q `1 )) "\/" a) "\/" b by A133, Def11;
then A135: (new_bi_fun d,q) . p,u <= ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" (a "\/" b) by A134, LATTICE3:14;
A136: ((d . p9,(q `2 )) "\/" a) "\/" (a "\/" b) = (((d . p9,(q `2 )) "\/" a) "\/" a) "\/" b by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" (a "\/" a)) "\/" b by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" a) "\/" b by YELLOW_5:1
.= ((d . p9,(q `2 )) "\/" b) "\/" a by LATTICE3:14 ;
A137: (new_bi_fun d,q) . p,q = (d . p9,(q `2 )) "\/" b by A133, Def11;
A138: (d . p9,(q `2 )) "\/" (a "\/" b) <= (d . p9,(q `2 )) "\/" (a "\/" b) ;
( d . (q `2 ),(q `1 ) <= a "\/" b & ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" (a "\/" b) = ((d . p9,(q `2 )) "\/" (a "\/" b)) "\/" (d . (q `2 ),(q `1 )) ) by A1, A14, Def6, LATTICE3:14;
then A139: ((d . p9,(q `2 )) "\/" (d . (q `2 ),(q `1 ))) "\/" (a "\/" b) <= ((d . p9,(q `2 )) "\/" (a "\/" b)) "\/" (a "\/" b) by A138, YELLOW_3:3;
((d . p9,(q `2 )) "\/" a) "\/" (a "\/" b) = ((d . p9,(q `2 )) "\/" a) "\/" ((a "\/" b) "\/" (a "\/" b)) by YELLOW_5:1
.= (d . p9,(q `2 )) "\/" (a "\/" ((a "\/" b) "\/" (a "\/" b))) by LATTICE3:14
.= (d . p9,(q `2 )) "\/" ((a "\/" (a "\/" b)) "\/" (a "\/" b)) by LATTICE3:14
.= (d . p9,(q `2 )) "\/" (((a "\/" a) "\/" b) "\/" (a "\/" b)) by LATTICE3:14
.= (d . p9,(q `2 )) "\/" ((a "\/" b) "\/" (a "\/" b)) by YELLOW_5:1
.= ((d . p9,(q `2 )) "\/" (a "\/" b)) "\/" (a "\/" b) by LATTICE3:14 ;
then (new_bi_fun d,q) . p,u <= ((d . p9,(q `2 )) "\/" a) "\/" (a "\/" b) by A139, A135, ORDERS_2:26;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A133, A137, A136, Def11; :: thesis: verum

end;

suppose A140: ( p in A & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

then ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun d,q) . p,q) by Def11
.= (new_bi_fun d,q) . p,q by WAYBEL_1:4 ;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A140; :: thesis: verum

end;

end;

end;

A141: for p, q, u being Element of new_set A st p in A & q in A & u in A holds
(new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: ( p in A & q in A & u in A implies (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) )
assume ( p in A & q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)
then reconsider p9 = p, q9 = q, u9 = u as Element of A ;
A142: (new_bi_fun d,q) . q,u = d . q9,u9 by Def11;
( (new_bi_fun d,q) . p,u = d . p9,u9 & (new_bi_fun d,q) . p,q = d . p9,q9 ) by Def11;
hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A2, A142, Def8; :: thesis: verum

end;

for p, q, u being Element of new_set A holds (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

proof

let p, q, u be Element of new_set A; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

per cases ( ( p in A & q in A & u in A ) or ( p in A & q in A & u in B ) or ( p in A & q in B & u in A ) or ( p in A & q in B & u in B ) or ( p in B & q in A & u in A ) or ( p in B & q in A & u in B ) or ( p in B & q in B & u in A ) or ( p in B & q in B & u in B ) ) by XBOOLE_0:def 3;

suppose ( p in A & q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A141; :: thesis: verum

end;

suppose ( p in A & q in A & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A54; :: thesis: verum

end;

suppose ( p in A & q in B & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A3; :: thesis: verum

end;

suppose ( p in A & q in B & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A114; :: thesis: verum

end;

suppose ( p in B & q in A & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A42; :: thesis: verum

end;

suppose ( p in B & q in A & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A98; :: thesis: verum

end;

suppose ( p in B & q in B & u in A ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A15; :: thesis: verum

end;

suppose ( p in B & q in B & u in B ) ; :: thesis: (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u)

hence (new_bi_fun d,q) . p,u <= ((new_bi_fun d,q) . p,q) "\/" ((new_bi_fun d,q) . q,u) by A65; :: thesis: verum

end;

end;

end;

hence new_bi_fun d,q is u.t.i. by Def8; :: thesis: verum