let A be non empty set ; :: thesis: for L being lower-bounded LATTICE st L is modular holds
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_fun2 d,q is u.t.i.
let L be lower-bounded LATTICE; :: thesis: ( L is modular implies 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_fun2 d,q is u.t.i. )
assume A1: L is modular ; :: 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_fun2 d,q is u.t.i.
reconsider B = {{A},{{A}}} as non empty set ;
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_fun2 d,q is u.t.i. )
assume that
A2: d is symmetric and
A3: 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_fun2 d,q is u.t.i.
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_fun2 d,q is u.t.i. )
set x = q `1 ;
set y = q `2 ;
set a = q `3 ;
set b = q `4 ;
set f = new_bi_fun2 d,q;
reconsider a = q `3 , b = q `4 as Element of L ;
A4: for p, q, u being Element of new_set2 A st p in A & q in A & u in B holds
(new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u)

proof

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

per cases ( ( p in A & q in A & u = {A} ) or ( p in A & q in A & u = {{A}} ) ) by A5, TARSKI:def 2;

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

then reconsider p9 = p, q9 = q as Element of A ;
A7: (new_bi_fun2 d,q) . p,q = d . p9,q9 by Def5;
d . p9,(q `1 ) <= (d . p9,q9) "\/" (d . q9,(q `1 )) by A3, LATTICE5:def 8;
then A8: (d . p9,(q `1 )) "\/" a <= ((d . p9,q9) "\/" (d . q9,(q `1 ))) "\/" a by WAYBEL_1:3;
( (new_bi_fun2 d,q) . p,u = (d . p9,(q `1 )) "\/" a & (new_bi_fun2 d,q) . q,u = (d . q9,(q `1 )) "\/" a ) by A6, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A7, A8, LATTICE3:14; :: thesis: verum

end;

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

then reconsider p9 = p, q9 = q as Element of A ;
A10: (new_bi_fun2 d,q) . p,q = d . p9,q9 by Def5;
d . p9,(q `2 ) <= (d . p9,q9) "\/" (d . q9,(q `2 )) by A3, LATTICE5:def 8;
then A11: (d . p9,(q `2 )) "\/" a <= ((d . p9,q9) "\/" (d . q9,(q `2 ))) "\/" a by WAYBEL_1:3;
( (new_bi_fun2 d,q) . p,u = (d . p9,(q `2 )) "\/" a & (new_bi_fun2 d,q) . q,u = (d . q9,(q `2 )) "\/" a ) by A9, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A10, A11, LATTICE3:14; :: thesis: verum

end;

end;

end;

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

proof

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

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}} ) ) by A14, TARSKI:def 2;

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

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

end;

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

then reconsider p9 = p as Element of A ;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A17: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
d . p9,(q `2 ) <= (d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then A18: (d . p9,(q `2 )) "\/" a <= ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) <= ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A19: ( (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) & (d . p9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . p9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:3, YELLOW_5:2;
( (new_bi_fun2 d,q) . p,q = (d . p9,(q `1 )) "\/" a & (new_bi_fun2 d,q) . q,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b ) by A16, Def5;
then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . p9,(q `1 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A17, LATTICE3:14
.= (d . p9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . p9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . p9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A19, LATTICE3:14;
then (d . p9,(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A18, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A16, Def5; :: thesis: verum

end;

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

then reconsider p9 = p as Element of A ;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A21: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) <= ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A22: ( (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) & (d . p9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . p9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:3, YELLOW_5:2;
d . (q `2 ),(q `1 ) = d . (q `1 ),(q `2 ) by A2, LATTICE5:def 6;
then d . p9,(q `1 ) <= (d . p9,(q `2 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then A23: (d . p9,(q `1 )) "\/" a <= ((d . p9,(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
( (new_bi_fun2 d,q) . p,q = (d . p9,(q `2 )) "\/" a & (new_bi_fun2 d,q) . q,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b ) by A20, Def5;
then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . p9,(q `2 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A21, LATTICE3:14
.= (d . p9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . p9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . p9,(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A22, LATTICE3:14;
then (d . p9,(q `1 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A23, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A20, Def5; :: thesis: verum

end;

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

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

end;

end;

end;

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

proof

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

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}} ) ) by A26, TARSKI:def 2;

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

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

end;

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

then reconsider q9 = q as Element of A ;
d . q9,(q `1 ) = d . (q `1 ),q9 by A2, LATTICE5:def 6;
then A28: d . (q `1 ),(q `2 ) <= (d . q9,(q `1 )) "\/" (d . q9,(q `2 )) by A3, LATTICE5:def 8;
(new_bi_fun2 d,q) . p,q = (d . q9,(q `1 )) "\/" a by A27, Def5;
then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = ((d . q9,(q `1 )) "\/" a) "\/" ((d . q9,(q `2 )) "\/" a) by A27, Def5
.= ((d . q9,(q `1 )) "\/" ((d . q9,(q `2 )) "\/" a)) "\/" a by LATTICE3:14
.= (((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" a) "\/" a by LATTICE3:14
.= ((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" (a "\/" a) by LATTICE3:14
.= ((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" a by YELLOW_5:1 ;
then A29: (d . (q `1 ),(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A28, YELLOW_5:7;
A30: ((d . (q `1 ),(q `2 )) "\/" a) "/\" b <= (d . (q `1 ),(q `2 )) "\/" a by YELLOW_0:23;
(new_bi_fun2 d,q) . p,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A27, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A29, A30, ORDERS_2:26; :: thesis: verum

end;

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

then reconsider q9 = q as Element of A ;
d . q9,(q `1 ) = d . (q `1 ),q9 by A2, LATTICE5:def 6;
then A32: d . (q `1 ),(q `2 ) <= (d . q9,(q `1 )) "\/" (d . q9,(q `2 )) by A3, LATTICE5:def 8;
(new_bi_fun2 d,q) . p,q = (d . q9,(q `2 )) "\/" a by A31, Def5;
then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = ((d . q9,(q `1 )) "\/" a) "\/" ((d . q9,(q `2 )) "\/" a) by A31, Def5
.= ((d . q9,(q `1 )) "\/" ((d . q9,(q `2 )) "\/" a)) "\/" a by LATTICE3:14
.= (((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" a) "\/" a by LATTICE3:14
.= ((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" (a "\/" a) by LATTICE3:14
.= ((d . q9,(q `1 )) "\/" (d . q9,(q `2 ))) "\/" a by YELLOW_5:1 ;
then A33: (d . (q `1 ),(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A32, YELLOW_5:7;
A34: ((d . (q `1 ),(q `2 )) "\/" a) "/\" b <= (d . (q `1 ),(q `2 )) "\/" a by YELLOW_0:23;
(new_bi_fun2 d,q) . p,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A31, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A33, A34, ORDERS_2:26; :: thesis: verum

end;

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

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

end;

end;

end;

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

proof

let p, q, u be Element of new_set2 A; :: thesis: ( p in B & q in B & u in B implies (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) )
assume A36: ( p in B & q in B & u in B ) ; :: thesis: (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 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}} ) ) by A36, TARSKI:def 2;

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

Bottom L <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A37, Def5; :: thesis: verum

end;

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

then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun2 d,q) . p,u) by Def5
.= (Bottom L) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) by A38, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A38, Def5; :: thesis: verum

end;

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

Bottom L <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A39, Def5; :: thesis: verum

end;

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

then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) "\/" ((new_bi_fun2 d,q) . q,u) by Def5
.= (Bottom L) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) by A40, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A40, Def5; :: thesis: verum

end;

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

then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) "\/" ((new_bi_fun2 d,q) . q,u) by Def5
.= (Bottom L) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) by A41, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4
.= (new_bi_fun2 d,q) . p,q by A41, Def5 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A41; :: thesis: verum

end;

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

Bottom L <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A42, Def5; :: thesis: verum

end;

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

then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (Bottom L) "\/" ((new_bi_fun2 d,q) . p,u) by Def5
.= (Bottom L) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) by A43, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A43, Def5; :: thesis: verum

end;

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

Bottom L <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by YELLOW_0:44;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A44, Def5; :: thesis: verum

end;

end;

end;

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

proof

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

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}} ) ) by A46, TARSKI:def 2;

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

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

end;

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

then reconsider u9 = u as Element of A ;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A49: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
d . u9,(q `2 ) <= (d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then A50: (d . u9,(q `2 )) "\/" a <= ((d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) <= ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A51: ( (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) & (d . u9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . u9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:3, YELLOW_5:2;
( (new_bi_fun2 d,q) . p,q = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b & (new_bi_fun2 d,q) . q,u = (d . u9,(q `1 )) "\/" a ) by A48, Def5;
then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . u9,(q `1 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A49, LATTICE3:14
.= (d . u9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . u9,(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . u9,(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A51, LATTICE3:14;
then (d . u9,(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A50, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A48, Def5; :: thesis: verum

end;

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

then reconsider u9 = u as Element of A ;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A53: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) <= ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A54: ( (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) & (d . u9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . u9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:3, YELLOW_5:2;
d . (q `2 ),(q `1 ) = d . (q `1 ),(q `2 ) by A2, LATTICE5:def 6;
then d . u9,(q `1 ) <= (d . u9,(q `2 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then A55: (d . u9,(q `1 )) "\/" a <= ((d . u9,(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
( (new_bi_fun2 d,q) . p,q = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b & (new_bi_fun2 d,q) . q,u = (d . u9,(q `2 )) "\/" a ) by A52, Def5;
then ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . u9,(q `2 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A53, LATTICE3:14
.= (d . u9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . u9,(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . u9,(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A54, LATTICE3:14;
then (d . u9,(q `1 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A55, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A52, Def5; :: thesis: verum

end;

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

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

end;

end;

end;

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

proof

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

per cases ( ( p = {A} & q in A & u in A ) or ( p = {{A}} & q in A & u in A ) ) by A58, A59, TARSKI:def 2;

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

d . u9,(q `1 ) <= (d . u9,q9) "\/" (d . q9,(q `1 )) by A3, LATTICE5:def 8;
then d . u9,(q `1 ) <= (d . q9,u9) "\/" (d . q9,(q `1 )) by A2, LATTICE5:def 6;
then (d . u9,(q `1 )) "\/" a <= ((d . q9,(q `1 )) "\/" (d . q9,u9)) "\/" a by WAYBEL_1:3;
then A61: (d . u9,(q `1 )) "\/" a <= ((d . q9,(q `1 )) "\/" a) "\/" (d . q9,u9) by LATTICE3:14;
A62: (new_bi_fun2 d,q) . q,u = d . q9,u9 by Def5;
(new_bi_fun2 d,q) . p,q = (d . q9,(q `1 )) "\/" a by A60, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A60, A62, A61, Def5; :: thesis: verum

end;

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

d . u9,(q `2 ) <= (d . u9,q9) "\/" (d . q9,(q `2 )) by A3, LATTICE5:def 8;
then d . u9,(q `2 ) <= (d . q9,u9) "\/" (d . q9,(q `2 )) by A2, LATTICE5:def 6;
then (d . u9,(q `2 )) "\/" a <= ((d . q9,(q `2 )) "\/" (d . q9,u9)) "\/" a by WAYBEL_1:3;
then A64: (d . u9,(q `2 )) "\/" a <= ((d . q9,(q `2 )) "\/" a) "\/" (d . q9,u9) by LATTICE3:14;
A65: (new_bi_fun2 d,q) . q,u = d . q9,u9 by Def5;
(new_bi_fun2 d,q) . p,q = (d . q9,(q `2 )) "\/" a by A63, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A63, A65, A64, Def5; :: thesis: verum

end;

end;

end;

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

proof

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

per cases ( ( p in A & u in A & q = {A} ) or ( p in A & u in A & q = {{A}} ) ) by A67, TARSKI:def 2;

suppose A68: ( p in A & u in A & q = {A} ) ; :: thesis: (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 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 A3, LATTICE5:def 8;
then A69: ( (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 A2, LATTICE5:def 6, 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 A70: d . p9,u9 <= ((d . p9,(q `1 )) "\/" a) "\/" ((d . u9,(q `1 )) "\/" a) by A69, ORDERS_2:26;
( (new_bi_fun2 d,q) . p,q = (d . p9,(q `1 )) "\/" a & (new_bi_fun2 d,q) . q,u = (d . u9,(q `1 )) "\/" a ) by A68, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A70, Def5; :: thesis: verum

end;

suppose A71: ( p in A & u in A & q = {{A}} ) ; :: thesis: (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 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 A3, LATTICE5:def 8;
then A72: ( (d . p9,(q `2 )) "\/" (d . u9,(q `2 )) <= ((d . p9,(q `2 )) "\/" (d . u9,(q `2 ))) "\/" a & d . p9,u9 <= (d . p9,(q `2 )) "\/" (d . u9,(q `2 )) ) by A2, LATTICE5:def 6, YELLOW_0:22;
((d . p9,(q `2 )) "\/" (d . u9,(q `2 ))) "\/" a = (d . p9,(q `2 )) "\/" ((d . u9,(q `2 )) "\/" a) by LATTICE3:14
.= (d . p9,(q `2 )) "\/" ((d . u9,(q `2 )) "\/" (a "\/" a)) by YELLOW_5:1
.= (d . p9,(q `2 )) "\/" (((d . u9,(q `2 )) "\/" a) "\/" a) by LATTICE3:14
.= ((d . p9,(q `2 )) "\/" a) "\/" ((d . u9,(q `2 )) "\/" a) by LATTICE3:14 ;
then A73: d . p9,u9 <= ((d . p9,(q `2 )) "\/" a) "\/" ((d . u9,(q `2 )) "\/" a) by A72, ORDERS_2:26;
( (new_bi_fun2 d,q) . p,q = (d . p9,(q `2 )) "\/" a & (new_bi_fun2 d,q) . q,u = (d . u9,(q `2 )) "\/" a ) by A71, Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A73, Def5; :: thesis: verum

end;

end;

end;

A74: for p, q, u being Element of new_set2 A st p in A & q in A & u in A holds
(new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u)

proof

let p, q, u be Element of new_set2 A; :: thesis: ( p in A & q in A & u in A implies (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) )
assume ( p in A & q in A & u in A ) ; :: thesis: (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u)
then reconsider p9 = p, q9 = q, u9 = u as Element of A ;
A75: (new_bi_fun2 d,q) . q,u = d . q9,u9 by Def5;
( (new_bi_fun2 d,q) . p,u = d . p9,u9 & (new_bi_fun2 d,q) . p,q = d . p9,q9 ) by Def5;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A3, A75, LATTICE5:def 8; :: thesis: verum

end;

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

proof

let p, q, u be Element of new_set2 A; :: thesis: (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 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_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u)

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

hence new_bi_fun2 d,q is u.t.i. by LATTICE5:def 8; :: thesis: verum