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 7;
then A8: (d . (p9,(q `1))) "\/" a <= ((d . (p9,q9)) "\/" (d . (q9,(q `1)))) "\/" a by WAYBEL_1:2;
( (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 7;
then A11: (d . (p9,(q `2))) "\/" a <= ((d . (p9,q9)) "\/" (d . (q9,(q `2)))) "\/" a by WAYBEL_1:2;
( (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:3 ;
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 7;
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:2, 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:3;
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:2, YELLOW_5:2;
d . ((q `2),(q `1)) = d . ((q `1),(q `2)) by A2, LATTICE5:def 5;
then d . (p9,(q `1)) <= (d . (p9,(q `2))) "\/" (d . ((q `1),(q `2))) by A3, LATTICE5:def 7;
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:3;
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:3 ;
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 5;
then A28: d . ((q `1),(q `2)) <= (d . (q9,(q `1))) "\/" (d . (q9,(q `2))) by A3, LATTICE5:def 7;
(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:3; :: 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 5;
then A32: d . ((q `1),(q `2)) <= (d . (q9,(q `1))) "\/" (d . (q9,(q `2))) by A3, LATTICE5:def 7;
(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:3; :: 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:3 ;
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:3 ;
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:3
.= (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:3 ;
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:3 ;
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 7;
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:2, 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:3;
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:2, YELLOW_5:2;
d . ((q `2),(q `1)) = d . ((q `1),(q `2)) by A2, LATTICE5:def 5;
then d . (u9,(q `1)) <= (d . (u9,(q `2))) "\/" (d . ((q `1),(q `2))) by A3, LATTICE5:def 7;
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:3;
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:3 ;
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 7;
then d . (u9,(q `1)) <= (d . (q9,u9)) "\/" (d . (q9,(q `1))) by A2, LATTICE5:def 5;
then (d . (u9,(q `1))) "\/" a <= ((d . (q9,(q `1))) "\/" (d . (q9,u9))) "\/" a by WAYBEL_1:2;
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 7;
then d . (u9,(q `2)) <= (d . (q9,u9)) "\/" (d . (q9,(q `2))) by A2, LATTICE5:def 5;
then (d . (u9,(q `2))) "\/" a <= ((d . (q9,(q `2))) "\/" (d . (q9,u9))) "\/" a by WAYBEL_1:2;
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 7;
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 5, 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:3;
( (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 7;
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 5, 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:3;
( (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 7; :: 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 7; :: thesis: verum