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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) implies new_bi_fun2 (d,q) is u.t.i. )
set x = q `1_4 ;
set y = q `2_4 ;
set a = q `3_4 ;
set b = q `4_4 ;
set f = new_bi_fun2 (d,q);
reconsider a = q `3_4 , b = q `4_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 Def4;
d . (p9,(q `1_4)) <= (d . (p9,q9)) "\/" (d . (q9,(q `1_4))) by A3;
then A8: (d . (p9,(q `1_4))) "\/" a <= ((d . (p9,q9)) "\/" (d . (q9,(q `1_4)))) "\/" a by WAYBEL_1:2;
( (new_bi_fun2 (d,q)) . (p,u) = (d . (p9,(q `1_4))) "\/" a & (new_bi_fun2 (d,q)) . (q,u) = (d . (q9,(q `1_4))) "\/" a ) by A6, Def4;
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 Def4;
d . (p9,(q `2_4)) <= (d . (p9,q9)) "\/" (d . (q9,(q `2_4))) by A3;
then A11: (d . (p9,(q `2_4))) "\/" a <= ((d . (p9,q9)) "\/" (d . (q9,(q `2_4)))) "\/" a by WAYBEL_1:2;
( (new_bi_fun2 (d,q)) . (p,u) = (d . (p9,(q `2_4))) "\/" a & (new_bi_fun2 (d,q)) . (q,u) = (d . (q9,(q `2_4))) "\/" a ) by A9, Def4;
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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_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 Def4
.= (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_4),(q `2_4))) by YELLOW_0:22;
then A17: a "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4)))) by A1;
d . (p9,(q `2_4)) <= (d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4))) by A3;
then A18: (d . (p9,(q `2_4))) "\/" a <= ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a by YELLOW_5:7;
a <= a ;
then (d . ((q `1_4),(q `2_4))) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) <= ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A19: ( (d . ((q `1_4),(q `2_4))) "\/" a = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) & (d . (p9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a)) <= (d . (p9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:2, YELLOW_5:2;
( (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `1_4))) "\/" a & (new_bi_fun2 (d,q)) . (q,u) = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b ) by A16, Def4;
then ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) = (d . (p9,(q `1_4))) "\/" ((a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4))))) by A17, LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A19, LATTICE3:14;
then (d . (p9,(q `2_4))) "\/" 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, Def4; :: 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_4),(q `2_4))) by YELLOW_0:22;
then A21: a "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4)))) by A1;
a <= a ;
then (d . ((q `1_4),(q `2_4))) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) <= ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A22: ( (d . ((q `1_4),(q `2_4))) "\/" a = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) & (d . (p9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a)) <= (d . (p9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:2, YELLOW_5:2;
d . ((q `2_4),(q `1_4)) = d . ((q `1_4),(q `2_4)) by A2;
then d . (p9,(q `1_4)) <= (d . (p9,(q `2_4))) "\/" (d . ((q `1_4),(q `2_4))) by A3;
then A23: (d . (p9,(q `1_4))) "\/" a <= ((d . (p9,(q `2_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a by YELLOW_5:7;
( (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" a & (new_bi_fun2 (d,q)) . (q,u) = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b ) by A20, Def4;
then ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) = (d . (p9,(q `2_4))) "\/" ((a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4))))) by A21, LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . (p9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . (p9,(q `2_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A22, LATTICE3:14;
then (d . (p9,(q `1_4))) "\/" 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, Def4; :: 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 Def4
.= (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 Def4;
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_4)) = d . ((q `1_4),q9) by A2;
then A28: d . ((q `1_4),(q `2_4)) <= (d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4))) by A3;
(new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `1_4))) "\/" a by A27, Def4;
then ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) = ((d . (q9,(q `1_4))) "\/" a) "\/" ((d . (q9,(q `2_4))) "\/" a) by A27, Def4
.= ((d . (q9,(q `1_4))) "\/" ((d . (q9,(q `2_4))) "\/" a)) "\/" a by LATTICE3:14
.= (((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" a) "\/" a by LATTICE3:14
.= ((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" (a "\/" a) by LATTICE3:14
.= ((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" a by YELLOW_5:1 ;
then A29: (d . ((q `1_4),(q `2_4))) "\/" a <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A28, YELLOW_5:7;
A30: ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b <= (d . ((q `1_4),(q `2_4))) "\/" a by YELLOW_0:23;
(new_bi_fun2 (d,q)) . (p,u) = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b by A27, Def4;
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_4)) = d . ((q `1_4),q9) by A2;
then A32: d . ((q `1_4),(q `2_4)) <= (d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4))) by A3;
(new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `2_4))) "\/" a by A31, Def4;
then ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) = ((d . (q9,(q `1_4))) "\/" a) "\/" ((d . (q9,(q `2_4))) "\/" a) by A31, Def4
.= ((d . (q9,(q `1_4))) "\/" ((d . (q9,(q `2_4))) "\/" a)) "\/" a by LATTICE3:14
.= (((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" a) "\/" a by LATTICE3:14
.= ((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" (a "\/" a) by LATTICE3:14
.= ((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" a by YELLOW_5:1 ;
then A33: (d . ((q `1_4),(q `2_4))) "\/" a <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A32, YELLOW_5:7;
A34: ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b <= (d . ((q `1_4),(q `2_4))) "\/" a by YELLOW_0:23;
(new_bi_fun2 (d,q)) . (p,u) = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b by A31, Def4;
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 Def4;
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, Def4; :: 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 Def4
.= (Bottom L) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) by A38, Def4
.= ((d . ((q `1_4),(q `2_4))) "\/" 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, Def4; :: 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, Def4; :: 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_4),(q `2_4))) "\/" a) "/\" b) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by Def4
.= (Bottom L) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) by A40, Def4
.= ((d . ((q `1_4),(q `2_4))) "\/" 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, Def4; :: 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_4),(q `2_4))) "\/" a) "/\" b) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by Def4
.= (Bottom L) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) by A41, Def4
.= ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b by WAYBEL_1:3
.= (new_bi_fun2 (d,q)) . (p,q) by A41, Def4 ;
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, Def4; :: 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 Def4
.= (Bottom L) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) by A43, Def4
.= ((d . ((q `1_4),(q `2_4))) "\/" 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, Def4; :: 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, Def4; :: 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 Def4
.= (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_4),(q `2_4))) by YELLOW_0:22;
then A49: a "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4)))) by A1;
d . (u9,(q `2_4)) <= (d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4))) by A3;
then A50: (d . (u9,(q `2_4))) "\/" a <= ((d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a by YELLOW_5:7;
a <= a ;
then (d . ((q `1_4),(q `2_4))) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) <= ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A51: ( (d . ((q `1_4),(q `2_4))) "\/" a = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) & (d . (u9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a)) <= (d . (u9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:2, YELLOW_5:2;
( (new_bi_fun2 (d,q)) . (p,q) = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b & (new_bi_fun2 (d,q)) . (q,u) = (d . (u9,(q `1_4))) "\/" a ) by A48, Def4;
then ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) = (d . (u9,(q `1_4))) "\/" ((a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4))))) by A49, LATTICE3:14
.= (d . (u9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . (u9,(q `1_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A51, LATTICE3:14;
then (d . (u9,(q `2_4))) "\/" 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, Def4; :: 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_4),(q `2_4))) by YELLOW_0:22;
then A53: a "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4)))) by A1;
a <= a ;
then (d . ((q `1_4),(q `2_4))) "\/" a <= (a "\/" b) "\/" a by A12, YELLOW_3:3;
then ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) <= ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a) by YELLOW_5:6;
then A54: ( (d . ((q `1_4),(q `2_4))) "\/" a = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a) & (d . (u9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((d . ((q `1_4),(q `2_4))) "\/" a)) <= (d . (u9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) ) by WAYBEL_1:2, YELLOW_5:2;
d . ((q `2_4),(q `1_4)) = d . ((q `1_4),(q `2_4)) by A2;
then d . (u9,(q `1_4)) <= (d . (u9,(q `2_4))) "\/" (d . ((q `1_4),(q `2_4))) by A3;
then A55: (d . (u9,(q `1_4))) "\/" a <= ((d . (u9,(q `2_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a by YELLOW_5:7;
( (new_bi_fun2 (d,q)) . (p,q) = ((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b & (new_bi_fun2 (d,q)) . (q,u) = (d . (u9,(q `2_4))) "\/" a ) by A52, Def4;
then ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) = (d . (u9,(q `2_4))) "\/" ((a "\/" b) "/\" (a "\/" (d . ((q `1_4),(q `2_4))))) by A53, LATTICE3:14
.= (d . (u9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . (u9,(q `2_4))) "\/" (((d . ((q `1_4),(q `2_4))) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then ((d . (u9,(q `2_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" a <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A54, LATTICE3:14;
then (d . (u9,(q `1_4))) "\/" 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, Def4; :: 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 Def4
.= (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_4)) <= (d . (u9,q9)) "\/" (d . (q9,(q `1_4))) by A3;
then d . (u9,(q `1_4)) <= (d . (q9,u9)) "\/" (d . (q9,(q `1_4))) by A2;
then (d . (u9,(q `1_4))) "\/" a <= ((d . (q9,(q `1_4))) "\/" (d . (q9,u9))) "\/" a by WAYBEL_1:2;
then A61: (d . (u9,(q `1_4))) "\/" a <= ((d . (q9,(q `1_4))) "\/" a) "\/" (d . (q9,u9)) by LATTICE3:14;
A62: (new_bi_fun2 (d,q)) . (q,u) = d . (q9,u9) by Def4;
(new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `1_4))) "\/" a by A60, Def4;
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, Def4; :: 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_4)) <= (d . (u9,q9)) "\/" (d . (q9,(q `2_4))) by A3;
then d . (u9,(q `2_4)) <= (d . (q9,u9)) "\/" (d . (q9,(q `2_4))) by A2;
then (d . (u9,(q `2_4))) "\/" a <= ((d . (q9,(q `2_4))) "\/" (d . (q9,u9))) "\/" a by WAYBEL_1:2;
then A64: (d . (u9,(q `2_4))) "\/" a <= ((d . (q9,(q `2_4))) "\/" a) "\/" (d . (q9,u9)) by LATTICE3:14;
A65: (new_bi_fun2 (d,q)) . (q,u) = d . (q9,u9) by Def4;
(new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `2_4))) "\/" a by A63, Def4;
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, Def4; :: 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_4))) "\/" (d . ((q `1_4),u9)) by A3;
then A69: ( (d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4))) <= ((d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4)))) "\/" a & d . (p9,u9) <= (d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4))) ) by A2, YELLOW_0:22;
((d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4)))) "\/" a = (d . (p9,(q `1_4))) "\/" ((d . (u9,(q `1_4))) "\/" a) by LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" ((d . (u9,(q `1_4))) "\/" (a "\/" a)) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" (((d . (u9,(q `1_4))) "\/" a) "\/" a) by LATTICE3:14
.= ((d . (p9,(q `1_4))) "\/" a) "\/" ((d . (u9,(q `1_4))) "\/" a) by LATTICE3:14 ;
then A70: d . (p9,u9) <= ((d . (p9,(q `1_4))) "\/" a) "\/" ((d . (u9,(q `1_4))) "\/" a) by A69, ORDERS_2:3;
( (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `1_4))) "\/" a & (new_bi_fun2 (d,q)) . (q,u) = (d . (u9,(q `1_4))) "\/" a ) by A68, Def4;
hence (new_bi_fun2 (d,q)) . (p,u) <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A70, Def4; :: 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_4))) "\/" (d . ((q `2_4),u9)) by A3;
then A72: ( (d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4))) <= ((d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4)))) "\/" a & d . (p9,u9) <= (d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4))) ) by A2, YELLOW_0:22;
((d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4)))) "\/" a = (d . (p9,(q `2_4))) "\/" ((d . (u9,(q `2_4))) "\/" a) by LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" ((d . (u9,(q `2_4))) "\/" (a "\/" a)) by YELLOW_5:1
.= (d . (p9,(q `2_4))) "\/" (((d . (u9,(q `2_4))) "\/" a) "\/" a) by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" a) "\/" ((d . (u9,(q `2_4))) "\/" a) by LATTICE3:14 ;
then A73: d . (p9,u9) <= ((d . (p9,(q `2_4))) "\/" a) "\/" ((d . (u9,(q `2_4))) "\/" a) by A72, ORDERS_2:3;
( (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" a & (new_bi_fun2 (d,q)) . (q,u) = (d . (u9,(q `2_4))) "\/" a ) by A71, Def4;
hence (new_bi_fun2 (d,q)) . (p,u) <= ((new_bi_fun2 (d,q)) . (p,q)) "\/" ((new_bi_fun2 (d,q)) . (q,u)) by A73, Def4; :: 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 Def4;
( (new_bi_fun2 (d,q)) . (p,u) = d . (p9,u9) & (new_bi_fun2 (d,q)) . (p,q) = d . (p9,q9) ) by Def4;
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; :: 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. ; :: thesis: verum