let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds
new_bi_fun (d,q) is u.t.i.
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds
new_bi_fun (d,q) is u.t.i.
let d be BiFunction of A,L; :: thesis: ( d is symmetric & d is u.t.i. implies for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds
new_bi_fun (d,q) is u.t.i. )
assume that
A1: d is symmetric and
A2: d is u.t.i. ; :: thesis: for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds
new_bi_fun (d,q) is u.t.i.
reconsider B = {{A},{{A}},{{{A}}}} as non empty set ;
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: ( d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) implies new_bi_fun (d,q) is u.t.i. )
set x = q `1_4 ;
set y = q `2_4 ;
set f = new_bi_fun (d,q);
reconsider a = q `3_4 , b = q `4_4 as Element of L ;
A3: for p, q, u being Element of new_set A st p in A & q in B & u in A holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in A & q in B & u in A implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume A4: ( p in A & q in B & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
per cases ( ( p in A & u in A & q = {A} ) or ( p in A & u in A & q = {{A}} ) or ( p in A & u in A & q = {{{A}}} ) ) by A4, ENUMSET1:def 1;
suppose A5: ( p in A & u in A & q = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, u9 = u as Element of A ;
d . (p9,u9) <= (d . (p9,(q `1_4))) "\/" (d . ((q `1_4),u9)) by A2;
then A6: ( (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 A1, 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 A7: d . (p9,u9) <= ((d . (p9,(q `1_4))) "\/" a) "\/" ((d . (u9,(q `1_4))) "\/" a) by A6, ORDERS_2:3;
( (new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `1_4))) "\/" a & (new_bi_fun (d,q)) . (q,u) = (d . (u9,(q `1_4))) "\/" a ) by A5, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A7, Def10; :: thesis: verum
end;
suppose A8: ( p in A & u in A & q = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, u9 = u as Element of A ;
d . (p9,u9) <= (d . (p9,(q `1_4))) "\/" (d . ((q `1_4),u9)) by A2;
then A9: ( (d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4))) <= ((d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4)))) "\/" (a "\/" b) & d . (p9,u9) <= (d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4))) ) by A1, YELLOW_0:22;
((d . (p9,(q `1_4))) "\/" (d . (u9,(q `1_4)))) "\/" (a "\/" b) = (d . (p9,(q `1_4))) "\/" ((d . (u9,(q `1_4))) "\/" (a "\/" b)) by LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" ((d . (u9,(q `1_4))) "\/" ((a "\/" b) "\/" (a "\/" b))) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" (((d . (u9,(q `1_4))) "\/" (a "\/" b)) "\/" (a "\/" b)) by LATTICE3:14
.= ((d . (p9,(q `1_4))) "\/" (a "\/" b)) "\/" ((d . (u9,(q `1_4))) "\/" (a "\/" b)) by LATTICE3:14
.= (((d . (p9,(q `1_4))) "\/" a) "\/" b) "\/" ((d . (u9,(q `1_4))) "\/" (a "\/" b)) by LATTICE3:14
.= (((d . (p9,(q `1_4))) "\/" a) "\/" b) "\/" (((d . (u9,(q `1_4))) "\/" a) "\/" b) by LATTICE3:14 ;
then A10: d . (p9,u9) <= (((d . (p9,(q `1_4))) "\/" a) "\/" b) "\/" (((d . (u9,(q `1_4))) "\/" a) "\/" b) by A9, ORDERS_2:3;
( (new_bi_fun (d,q)) . (p,q) = ((d . (p9,(q `1_4))) "\/" a) "\/" b & (new_bi_fun (d,q)) . (q,u) = ((d . (u9,(q `1_4))) "\/" a) "\/" b ) by A8, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A10, Def10; :: thesis: verum
end;
suppose A11: ( p in A & u in A & q = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, u9 = u as Element of A ;
d . (p9,u9) <= (d . (p9,(q `2_4))) "\/" (d . ((q `2_4),u9)) by A2;
then A12: ( (d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4))) <= ((d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4)))) "\/" b & d . (p9,u9) <= (d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4))) ) by A1, YELLOW_0:22;
((d . (p9,(q `2_4))) "\/" (d . (u9,(q `2_4)))) "\/" b = (d . (p9,(q `2_4))) "\/" ((d . (u9,(q `2_4))) "\/" b) by LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" ((d . (u9,(q `2_4))) "\/" (b "\/" b)) by YELLOW_5:1
.= (d . (p9,(q `2_4))) "\/" (((d . (u9,(q `2_4))) "\/" b) "\/" b) by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" b) "\/" ((d . (u9,(q `2_4))) "\/" b) by LATTICE3:14 ;
then A13: d . (p9,u9) <= ((d . (p9,(q `2_4))) "\/" b) "\/" ((d . (u9,(q `2_4))) "\/" b) by A12, ORDERS_2:3;
( (new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" b & (new_bi_fun (d,q)) . (q,u) = (d . (u9,(q `2_4))) "\/" b ) by A11, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A13, Def10; :: thesis: verum
end;
end;
end;
assume A14: d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) ; :: thesis: new_bi_fun (d,q) is u.t.i.
A15: for p, q, u being Element of new_set A st p in B & q in B & u in A holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in B & q in B & u in A implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume that
A16: ( p in B & q in B ) and
A17: u in A ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
reconsider u9 = u as Element of A by A17;
per cases ( ( u in A & q = {A} & p = {A} ) or ( u in A & q = {A} & p = {{A}} ) or ( u in A & q = {A} & p = {{{A}}} ) or ( u in A & q = {{A}} & p = {A} ) or ( u in A & q = {{A}} & p = {{A}} ) or ( u in A & q = {{A}} & p = {{{A}}} ) or ( u in A & q = {{{A}}} & p = {A} ) or ( u in A & q = {{{A}}} & p = {{A}} ) or ( u in A & q = {{{A}}} & p = {{{A}}} ) ) by A16, A17, ENUMSET1:def 1;
suppose A18: ( u in A & q = {A} & p = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (new_bi_fun (d,q)) . (p,u) by A18, WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) ; :: thesis: verum
end;
suppose A19: ( u in A & q = {A} & p = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = b "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= ((d . (u9,(q `1_4))) "\/" a) "\/" b by A19, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A19, Def10; :: thesis: verum
end;
suppose A20: ( u in A & q = {A} & p = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
b "\/" (a "\/" b) = (b "\/" b) "\/" a by LATTICE3:14
.= b "\/" a by YELLOW_5:1
.= b "\/" (a "\/" a) by YELLOW_5:1
.= a "\/" (a "\/" b) by LATTICE3:14 ;
then A21: ((d . (u9,(q `1_4))) "\/" b) "\/" (a "\/" b) = (d . (u9,(q `1_4))) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= (a "\/" b) "\/" ((d . (u9,(q `1_4))) "\/" a) by LATTICE3:14
.= ((new_bi_fun (d,q)) . (p,q)) "\/" ((d . (u9,(q `1_4))) "\/" a) by A20, Def10 ;
d . (u9,(q `2_4)) <= (d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4))) by A2;
then A22: (d . (u9,(q `2_4))) "\/" b <= ((d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b by WAYBEL_1:2;
(d . (u9,(q `1_4))) "\/" b <= (d . (u9,(q `1_4))) "\/" b ;
then A23: ( ((d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b = ((d . (u9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) & ((d . (u9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) <= ((d . (u9,(q `1_4))) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
(new_bi_fun (d,q)) . (p,u) = (d . (u9,(q `2_4))) "\/" b by A20, Def10;
then (new_bi_fun (d,q)) . (p,u) <= ((d . (u9,(q `1_4))) "\/" b) "\/" (a "\/" b) by A22, A23, ORDERS_2:3;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A20, A21, Def10; :: thesis: verum
end;
suppose A24: ( u in A & q = {{A}} & p = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = b "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= b "\/" (((d . (u9,(q `1_4))) "\/" a) "\/" b) by A24, Def10
.= b "\/" (b "\/" ((new_bi_fun (d,q)) . (p,u))) by A24, Def10
.= (b "\/" b) "\/" ((new_bi_fun (d,q)) . (p,u)) by LATTICE3:14
.= b "\/" ((new_bi_fun (d,q)) . (p,u)) by YELLOW_5:1 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:22; :: thesis: verum
end;
suppose A25: ( u in A & q = {{A}} & p = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (new_bi_fun (d,q)) . (p,u) by A25, WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) ; :: thesis: verum
end;
suppose A26: ( u in A & q = {{A}} & p = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
b "\/" (a "\/" b) = (b "\/" b) "\/" a by LATTICE3:14
.= b "\/" a by YELLOW_5:1
.= b "\/" (a "\/" a) by YELLOW_5:1
.= (a "\/" b) "\/" a by LATTICE3:14 ;
then A27: ((d . (u9,(q `1_4))) "\/" b) "\/" (a "\/" b) = (d . (u9,(q `1_4))) "\/" ((a "\/" b) "\/" a) by LATTICE3:14
.= ((d . (u9,(q `1_4))) "\/" (a "\/" b)) "\/" a by LATTICE3:14
.= (((d . (u9,(q `1_4))) "\/" a) "\/" b) "\/" a by LATTICE3:14
.= ((new_bi_fun (d,q)) . (p,q)) "\/" (((d . (u9,(q `1_4))) "\/" a) "\/" b) by A26, Def10 ;
(d . (u9,(q `1_4))) "\/" b <= (d . (u9,(q `1_4))) "\/" b ;
then A28: ( ((d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b = ((d . (u9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) & ((d . (u9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) <= ((d . (u9,(q `1_4))) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
d . (u9,(q `2_4)) <= (d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4))) by A2;
then A29: (d . (u9,(q `2_4))) "\/" b <= ((d . (u9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b by WAYBEL_1:2;
(new_bi_fun (d,q)) . (p,u) = (d . (u9,(q `2_4))) "\/" b by A26, Def10;
then (new_bi_fun (d,q)) . (p,u) <= ((d . (u9,(q `1_4))) "\/" b) "\/" (a "\/" b) by A29, A28, ORDERS_2:3;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A26, A27, Def10; :: thesis: verum
end;
suppose A30: ( u in A & q = {{{A}}} & p = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
A31: a "\/" (a "\/" b) = (a "\/" a) "\/" b by LATTICE3:14
.= a "\/" b by YELLOW_5:1
.= a "\/" (b "\/" b) by YELLOW_5:1
.= b "\/" (a "\/" b) by LATTICE3:14 ;
A32: (a "\/" (d . (u9,(q `2_4)))) "\/" (a "\/" b) = (d . (u9,(q `2_4))) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= ((d . (u9,(q `2_4))) "\/" b) "\/" (a "\/" b) by A31, LATTICE3:14
.= ((new_bi_fun (d,q)) . (p,q)) "\/" ((d . (u9,(q `2_4))) "\/" b) by A30, Def10 ;
a "\/" (d . (u9,(q `2_4))) <= a "\/" (d . (u9,(q `2_4))) ;
then A33: (a "\/" (d . (u9,(q `2_4)))) "\/" (d . ((q `1_4),(q `2_4))) <= (a "\/" (d . (u9,(q `2_4)))) "\/" (a "\/" b) by A14, YELLOW_3:3;
d . (u9,(q `1_4)) <= (d . (u9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4))) by A2;
then A34: (d . (u9,(q `1_4))) "\/" a <= ((d . (u9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" a by WAYBEL_1:2;
A35: ((d . (u9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" a = (d . ((q `2_4),(q `1_4))) "\/" ((d . (u9,(q `2_4))) "\/" a) by LATTICE3:14
.= (a "\/" (d . (u9,(q `2_4)))) "\/" (d . ((q `1_4),(q `2_4))) by A1 ;
(new_bi_fun (d,q)) . (p,u) = (d . (u9,(q `1_4))) "\/" a by A30, Def10;
then (new_bi_fun (d,q)) . (p,u) <= (a "\/" (d . (u9,(q `2_4)))) "\/" (a "\/" b) by A34, A35, A33, ORDERS_2:3;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A30, A32, Def10; :: thesis: verum
end;
suppose A36: ( u in A & q = {{{A}}} & p = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A37: (new_bi_fun (d,q)) . (p,u) = ((d . (u9,(q `1_4))) "\/" a) "\/" b by Def10
.= (d . (u9,(q `1_4))) "\/" (a "\/" b) by LATTICE3:14 ;
(a "\/" b) "\/" (d . (u9,(q `2_4))) <= (a "\/" b) "\/" (d . (u9,(q `2_4))) ;
then A38: ((a "\/" b) "\/" (d . (u9,(q `2_4)))) "\/" (d . ((q `1_4),(q `2_4))) <= ((a "\/" b) "\/" (d . (u9,(q `2_4)))) "\/" (a "\/" b) by A14, YELLOW_3:3;
d . (u9,(q `1_4)) <= (d . (u9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4))) by A2;
then A39: (d . (u9,(q `1_4))) "\/" (a "\/" b) <= ((d . (u9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" (a "\/" b) by WAYBEL_1:2;
A40: ((d . (u9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" (a "\/" b) = ((a "\/" b) "\/" (d . (u9,(q `2_4)))) "\/" (d . ((q `2_4),(q `1_4))) by LATTICE3:14
.= ((a "\/" b) "\/" (d . (u9,(q `2_4)))) "\/" (d . ((q `1_4),(q `2_4))) by A1 ;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = a "\/" ((new_bi_fun (d,q)) . (q,u)) by A36, Def10
.= a "\/" (b "\/" (d . (u9,(q `2_4)))) by A36, Def10
.= (a "\/" b) "\/" (d . (u9,(q `2_4))) by LATTICE3:14
.= ((a "\/" b) "\/" (a "\/" b)) "\/" (d . (u9,(q `2_4))) by YELLOW_5:1
.= (a "\/" b) "\/" ((d . (u9,(q `2_4))) "\/" (a "\/" b)) by LATTICE3:14 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A37, A39, A40, A38, ORDERS_2:3; :: thesis: verum
end;
suppose A41: ( u in A & q = {{{A}}} & p = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (new_bi_fun (d,q)) . (p,u) by A41, WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) ; :: thesis: verum
end;
end;
end;
A42: for p, q, u being Element of new_set A st p in B & q in A & u in A holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in B & q in A & u in A implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume that
A43: p in B and
A44: ( q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
reconsider q9 = q, u9 = u as Element of A by A44;
per cases ( ( p = {A} & q in A & u in A ) or ( p = {{A}} & q in A & u in A ) or ( p = {{{A}}} & q in A & u in A ) ) by A43, A44, ENUMSET1:def 1;
suppose A45: ( p = {A} & q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (u9,(q `1_4)) <= (d . (u9,q9)) "\/" (d . (q9,(q `1_4))) by A2;
then d . (u9,(q `1_4)) <= (d . (q9,u9)) "\/" (d . (q9,(q `1_4))) by A1;
then (d . (u9,(q `1_4))) "\/" a <= ((d . (q9,(q `1_4))) "\/" (d . (q9,u9))) "\/" a by WAYBEL_1:2;
then A46: (d . (u9,(q `1_4))) "\/" a <= ((d . (q9,(q `1_4))) "\/" a) "\/" (d . (q9,u9)) by LATTICE3:14;
A47: (new_bi_fun (d,q)) . (q,u) = d . (q9,u9) by Def10;
(new_bi_fun (d,q)) . (p,q) = (d . (q9,(q `1_4))) "\/" a by A45, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A45, A47, A46, Def10; :: thesis: verum
end;
suppose A48: ( p = {{A}} & q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (u9,(q `1_4)) <= (d . (u9,q9)) "\/" (d . (q9,(q `1_4))) by A2;
then d . (u9,(q `1_4)) <= (d . (q9,u9)) "\/" (d . (q9,(q `1_4))) by A1;
then (d . (u9,(q `1_4))) "\/" (a "\/" b) <= ((d . (q9,(q `1_4))) "\/" (d . (q9,u9))) "\/" (a "\/" b) by WAYBEL_1:2;
then ((d . (u9,(q `1_4))) "\/" a) "\/" b <= ((d . (q9,(q `1_4))) "\/" (d . (q9,u9))) "\/" (a "\/" b) by LATTICE3:14;
then ((d . (u9,(q `1_4))) "\/" a) "\/" b <= ((d . (q9,(q `1_4))) "\/" (a "\/" b)) "\/" (d . (q9,u9)) by LATTICE3:14;
then A49: ((d . (u9,(q `1_4))) "\/" a) "\/" b <= (((d . (q9,(q `1_4))) "\/" a) "\/" b) "\/" (d . (q9,u9)) by LATTICE3:14;
A50: (new_bi_fun (d,q)) . (q,u) = d . (q9,u9) by Def10;
(new_bi_fun (d,q)) . (p,q) = ((d . (q9,(q `1_4))) "\/" a) "\/" b by A48, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A48, A50, A49, Def10; :: thesis: verum
end;
suppose A51: ( p = {{{A}}} & q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (u9,(q `2_4)) <= (d . (u9,q9)) "\/" (d . (q9,(q `2_4))) by A2;
then d . (u9,(q `2_4)) <= (d . (q9,u9)) "\/" (d . (q9,(q `2_4))) by A1;
then (d . (u9,(q `2_4))) "\/" b <= ((d . (q9,(q `2_4))) "\/" (d . (q9,u9))) "\/" b by WAYBEL_1:2;
then A52: (d . (u9,(q `2_4))) "\/" b <= ((d . (q9,(q `2_4))) "\/" b) "\/" (d . (q9,u9)) by LATTICE3:14;
A53: (new_bi_fun (d,q)) . (q,u) = d . (q9,u9) by Def10;
(new_bi_fun (d,q)) . (p,q) = (d . (q9,(q `2_4))) "\/" b by A51, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A51, A53, A52, Def10; :: thesis: verum
end;
end;
end;
A54: for p, q, u being Element of new_set A st p in A & q in A & u in B holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in A & q in A & u in B implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume A55: ( p in A & q in A & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
per cases ( ( p in A & q in A & u = {A} ) or ( p in A & q in A & u = {{A}} ) or ( p in A & q in A & u = {{{A}}} ) ) by A55, ENUMSET1:def 1;
suppose A56: ( p in A & q in A & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, q9 = q as Element of A ;
A57: (new_bi_fun (d,q)) . (p,q) = d . (p9,q9) by Def10;
d . (p9,(q `1_4)) <= (d . (p9,q9)) "\/" (d . (q9,(q `1_4))) by A2;
then A58: (d . (p9,(q `1_4))) "\/" a <= ((d . (p9,q9)) "\/" (d . (q9,(q `1_4)))) "\/" a by WAYBEL_1:2;
( (new_bi_fun (d,q)) . (p,u) = (d . (p9,(q `1_4))) "\/" a & (new_bi_fun (d,q)) . (q,u) = (d . (q9,(q `1_4))) "\/" a ) by A56, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A57, A58, LATTICE3:14; :: thesis: verum
end;
suppose A59: ( p in A & q in A & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, q9 = q as Element of A ;
A60: (new_bi_fun (d,q)) . (p,q) = d . (p9,q9) by Def10;
d . (p9,(q `1_4)) <= (d . (p9,q9)) "\/" (d . (q9,(q `1_4))) by A2;
then (d . (p9,(q `1_4))) "\/" a <= ((d . (p9,q9)) "\/" (d . (q9,(q `1_4)))) "\/" a by WAYBEL_1:2;
then ((d . (p9,(q `1_4))) "\/" a) "\/" b <= (((d . (p9,q9)) "\/" (d . (q9,(q `1_4)))) "\/" a) "\/" b by WAYBEL_1:2;
then A61: ((d . (p9,(q `1_4))) "\/" a) "\/" b <= ((d . (p9,q9)) "\/" ((d . (q9,(q `1_4))) "\/" a)) "\/" b by LATTICE3:14;
( (new_bi_fun (d,q)) . (p,u) = ((d . (p9,(q `1_4))) "\/" a) "\/" b & (new_bi_fun (d,q)) . (q,u) = ((d . (q9,(q `1_4))) "\/" a) "\/" b ) by A59, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A60, A61, LATTICE3:14; :: thesis: verum
end;
suppose A62: ( p in A & q in A & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, q9 = q as Element of A ;
A63: (new_bi_fun (d,q)) . (p,q) = d . (p9,q9) by Def10;
d . (p9,(q `2_4)) <= (d . (p9,q9)) "\/" (d . (q9,(q `2_4))) by A2;
then A64: (d . (p9,(q `2_4))) "\/" b <= ((d . (p9,q9)) "\/" (d . (q9,(q `2_4)))) "\/" b by WAYBEL_1:2;
( (new_bi_fun (d,q)) . (p,u) = (d . (p9,(q `2_4))) "\/" b & (new_bi_fun (d,q)) . (q,u) = (d . (q9,(q `2_4))) "\/" b ) by A62, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A63, A64, LATTICE3:14; :: thesis: verum
end;
end;
end;
A65: for p, q, u being Element of new_set A st p in B & q in B & u in B holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in B & q in B & u in B implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume A66: ( p in B & q in B & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
per cases ( ( p = {A} & q = {A} & u = {A} ) or ( p = {A} & q = {A} & u = {{A}} ) or ( p = {A} & q = {A} & u = {{{A}}} ) or ( p = {A} & q = {{A}} & u = {A} ) or ( p = {A} & q = {{A}} & u = {{A}} ) or ( p = {A} & q = {{A}} & u = {{{A}}} ) or ( p = {A} & q = {{{A}}} & u = {A} ) or ( p = {A} & q = {{{A}}} & u = {{A}} ) or ( p = {A} & q = {{{A}}} & u = {{{A}}} ) or ( p = {{A}} & q = {A} & u = {A} ) or ( p = {{A}} & q = {A} & u = {{A}} ) or ( p = {{A}} & q = {A} & u = {{{A}}} ) or ( p = {{A}} & q = {{A}} & u = {A} ) or ( p = {{A}} & q = {{A}} & u = {{A}} ) or ( p = {{A}} & q = {{A}} & u = {{{A}}} ) or ( p = {{A}} & q = {{{A}}} & u = {A} ) or ( p = {{A}} & q = {{{A}}} & u = {{A}} ) or ( p = {{A}} & q = {{{A}}} & u = {{{A}}} ) or ( p = {{{A}}} & q = {A} & u = {A} ) or ( p = {{{A}}} & q = {A} & u = {{A}} ) or ( p = {{{A}}} & q = {A} & u = {{{A}}} ) or ( p = {{{A}}} & q = {{A}} & u = {A} ) or ( p = {{{A}}} & q = {{A}} & u = {{A}} ) or ( p = {{{A}}} & q = {{A}} & u = {{{A}}} ) or ( p = {{{A}}} & q = {{{A}}} & u = {A} ) or ( p = {{{A}}} & q = {{{A}}} & u = {{A}} ) or ( p = {{{A}}} & q = {{{A}}} & u = {{{A}}} ) ) by A66, ENUMSET1:def 1;
suppose A67: ( p = {A} & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A67, Def10; :: thesis: verum
end;
suppose A68: ( p = {A} & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,u)) by Def10
.= (Bottom L) "\/" b by A68, Def10
.= b by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A68, Def10; :: thesis: verum
end;
suppose A69: ( p = {A} & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,u)) by Def10
.= (Bottom L) "\/" (a "\/" b) by A69, Def10
.= a "\/" b by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A69, Def10; :: thesis: verum
end;
suppose A70: ( p = {A} & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A70, Def10; :: thesis: verum
end;
suppose A71: ( p = {A} & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = b "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (Bottom L) "\/" b by A71, Def10
.= b by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A71, Def10; :: thesis: verum
end;
suppose A72: ( p = {A} & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = b "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= a "\/" b by A72, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A72, Def10; :: thesis: verum
end;
suppose A73: ( p = {A} & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A73, Def10; :: thesis: verum
end;
suppose A74: ( p = {A} & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A75: (new_bi_fun (d,q)) . (p,u) = b by Def10;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (a "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by A74, Def10
.= (b "\/" a) "\/" a by A74, Def10
.= b "\/" (a "\/" a) by LATTICE3:14
.= b "\/" a by YELLOW_5:1 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A75, YELLOW_0:22; :: thesis: verum
end;
suppose A76: ( p = {A} & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (a "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (Bottom L) "\/" (a "\/" b) by A76, Def10
.= a "\/" b by WAYBEL_1:3
.= (new_bi_fun (d,q)) . (p,q) by A76, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A76; :: thesis: verum
end;
suppose A77: ( p = {{A}} & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = b "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (Bottom L) "\/" b by A77, Def10
.= b by WAYBEL_1:3
.= (new_bi_fun (d,q)) . (p,q) by A77, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A77; :: thesis: verum
end;
suppose A78: ( p = {{A}} & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A78, Def10; :: thesis: verum
end;
suppose A79: ( p = {{A}} & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A80: (new_bi_fun (d,q)) . (p,u) = a by Def10;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = b "\/" ((new_bi_fun (d,q)) . (q,u)) by A79, Def10
.= b "\/" (b "\/" a) by A79, Def10
.= (b "\/" b) "\/" a by LATTICE3:14
.= b "\/" a by YELLOW_5:1 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A80, YELLOW_0:22; :: thesis: verum
end;
suppose A81: ( p = {{A}} & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,u)) by Def10
.= (Bottom L) "\/" b by A81, Def10
.= b by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A81, Def10; :: thesis: verum
end;
suppose A82: ( p = {{A}} & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A82, Def10; :: thesis: verum
end;
suppose A83: ( p = {{A}} & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,u)) by Def10
.= (Bottom L) "\/" a by A83, Def10
.= a by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A83, Def10; :: thesis: verum
end;
suppose A84: ( p = {{A}} & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A85: (new_bi_fun (d,q)) . (p,u) = b by Def10;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = a "\/" ((new_bi_fun (d,q)) . (q,u)) by A84, Def10
.= a "\/" (a "\/" b) by A84, Def10
.= (a "\/" a) "\/" b by LATTICE3:14
.= a "\/" b by YELLOW_5:1 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A85, YELLOW_0:22; :: thesis: verum
end;
suppose A86: ( p = {{A}} & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A86, Def10; :: thesis: verum
end;
suppose A87: ( p = {{A}} & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = a "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (Bottom L) "\/" a by A87, Def10
.= a by WAYBEL_1:3
.= (new_bi_fun (d,q)) . (p,q) by A87, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A87; :: thesis: verum
end;
suppose A88: ( p = {{{A}}} & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (a "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (Bottom L) "\/" (a "\/" b) by A88, Def10
.= a "\/" b by WAYBEL_1:3
.= (new_bi_fun (d,q)) . (p,q) by A88, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A88; :: thesis: verum
end;
suppose A89: ( p = {{{A}}} & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A90: (new_bi_fun (d,q)) . (p,u) = a by Def10;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (a "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by A89, Def10
.= (a "\/" b) "\/" b by A89, Def10
.= a "\/" (b "\/" b) by LATTICE3:14
.= a "\/" b by YELLOW_5:1 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A90, YELLOW_0:22; :: thesis: verum
end;
suppose A91: ( p = {{{A}}} & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A91, Def10; :: thesis: verum
end;
suppose A92: ( p = {{{A}}} & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = a "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= a "\/" b by A92, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A92, Def10; :: thesis: verum
end;
suppose A93: ( p = {{{A}}} & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = a "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (Bottom L) "\/" a by A93, Def10
.= a by WAYBEL_1:3
.= (new_bi_fun (d,q)) . (p,q) by A93, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A93; :: thesis: verum
end;
suppose A94: ( p = {{{A}}} & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A94, Def10; :: thesis: verum
end;
suppose A95: ( p = {{{A}}} & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,u)) by Def10
.= (Bottom L) "\/" (a "\/" b) by A95, Def10
.= a "\/" b by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A95, Def10; :: thesis: verum
end;
suppose A96: ( p = {{{A}}} & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,u)) by Def10
.= (Bottom L) "\/" a by A96, Def10
.= a by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A96, Def10; :: thesis: verum
end;
suppose A97: ( p = {{{A}}} & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
Bottom L <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A97, Def10; :: thesis: verum
end;
end;
end;
A98: for p, q, u being Element of new_set A st p in B & q in A & u in B holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in B & q in A & u in B implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume that
A99: p in B and
A100: q in A and
A101: u in B ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
reconsider q9 = q as Element of A by A100;
per cases ( ( q in A & p = {A} & u = {A} ) or ( q in A & p = {A} & u = {{A}} ) or ( q in A & p = {A} & u = {{{A}}} ) or ( q in A & p = {{A}} & u = {A} ) or ( q in A & p = {{A}} & u = {{A}} ) or ( q in A & p = {{A}} & u = {{{A}}} ) or ( q in A & p = {{{A}}} & u = {A} ) or ( q in A & p = {{{A}}} & u = {{A}} ) or ( q in A & p = {{{A}}} & u = {{{A}}} ) ) by A99, A100, A101, ENUMSET1:def 1;
suppose ( q in A & p = {A} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then (new_bi_fun (d,q)) . (p,u) = Bottom L by Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44; :: thesis: verum
end;
suppose A102: ( q in A & p = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A103: ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = ((new_bi_fun (d,q)) . (p,q)) "\/" (((d . (q9,(q `1_4))) "\/" a) "\/" b) by Def10
.= ((new_bi_fun (d,q)) . (p,q)) "\/" ((d . (q9,(q `1_4))) "\/" (a "\/" b)) by LATTICE3:14
.= (((new_bi_fun (d,q)) . (p,q)) "\/" (d . (q9,(q `1_4)))) "\/" (a "\/" b) by LATTICE3:14
.= ((((new_bi_fun (d,q)) . (p,q)) "\/" (d . (q9,(q `1_4)))) "\/" a) "\/" b by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,u) = b by A102, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A103, YELLOW_0:22; :: thesis: verum
end;
suppose A104: ( q in A & p = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A105: (new_bi_fun (d,q)) . (p,u) = a "\/" b by Def10;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = ((d . (q9,(q `1_4))) "\/" a) "\/" ((new_bi_fun (d,q)) . (q,u)) by A104, Def10
.= ((d . (q9,(q `1_4))) "\/" a) "\/" ((d . (q9,(q `2_4))) "\/" b) by A104, Def10
.= (d . (q9,(q `1_4))) "\/" (a "\/" ((d . (q9,(q `2_4))) "\/" b)) by LATTICE3:14
.= (d . (q9,(q `1_4))) "\/" ((d . (q9,(q `2_4))) "\/" (a "\/" b)) by LATTICE3:14
.= ((d . (q9,(q `1_4))) "\/" (d . (q9,(q `2_4)))) "\/" (a "\/" b) by LATTICE3:14 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A105, YELLOW_0:22; :: thesis: verum
end;
suppose A106: ( q in A & p = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A107: ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (((d . (q9,(q `1_4))) "\/" a) "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= ((new_bi_fun (d,q)) . (q,u)) "\/" ((d . (q9,(q `1_4))) "\/" (a "\/" b)) by LATTICE3:14
.= (((new_bi_fun (d,q)) . (q,u)) "\/" (d . (q9,(q `1_4)))) "\/" (a "\/" b) by LATTICE3:14
.= ((((new_bi_fun (d,q)) . (q,u)) "\/" (d . (q9,(q `1_4)))) "\/" a) "\/" b by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,u) = b by A106, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A107, YELLOW_0:22; :: thesis: verum
end;
suppose ( q in A & p = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then (new_bi_fun (d,q)) . (p,u) = Bottom L by Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44; :: thesis: verum
end;
suppose A108: ( q in A & p = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A109: ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (((d . (q9,(q `1_4))) "\/" a) "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by Def10
.= (a "\/" ((d . (q9,(q `1_4))) "\/" b)) "\/" ((new_bi_fun (d,q)) . (q,u)) by LATTICE3:14
.= a "\/" (((d . (q9,(q `1_4))) "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u))) by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,u) = a by A108, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A109, YELLOW_0:22; :: thesis: verum
end;
suppose A110: ( q in A & p = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A111: (new_bi_fun (d,q)) . (p,u) = a "\/" b by Def10;
((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = ((d . (q9,(q `2_4))) "\/" b) "\/" ((new_bi_fun (d,q)) . (q,u)) by A110, Def10
.= ((d . (q9,(q `2_4))) "\/" b) "\/" ((d . (q9,(q `1_4))) "\/" a) by A110, Def10
.= (d . (q9,(q `2_4))) "\/" (b "\/" ((d . (q9,(q `1_4))) "\/" a)) by LATTICE3:14
.= (d . (q9,(q `2_4))) "\/" ((d . (q9,(q `1_4))) "\/" (b "\/" a)) by LATTICE3:14
.= ((d . (q9,(q `2_4))) "\/" (d . (q9,(q `1_4)))) "\/" (a "\/" b) by LATTICE3:14 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A111, YELLOW_0:22; :: thesis: verum
end;
suppose A112: ( q in A & p = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then A113: ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = ((new_bi_fun (d,q)) . (p,q)) "\/" (((d . (q9,(q `1_4))) "\/" a) "\/" b) by Def10
.= ((new_bi_fun (d,q)) . (p,q)) "\/" ((d . (q9,(q `1_4))) "\/" (a "\/" b)) by LATTICE3:14
.= (((new_bi_fun (d,q)) . (p,q)) "\/" (d . (q9,(q `1_4)))) "\/" (a "\/" b) by LATTICE3:14
.= ((((new_bi_fun (d,q)) . (p,q)) "\/" (d . (q9,(q `1_4)))) "\/" b) "\/" a by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,u) = a by A112, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A113, YELLOW_0:22; :: thesis: verum
end;
suppose ( q in A & p = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then (new_bi_fun (d,q)) . (p,u) = Bottom L by Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:44; :: thesis: verum
end;
end;
end;
A114: for p, q, u being Element of new_set A st p in A & q in B & u in B holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in A & q in B & u in B implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume that
A115: p in A and
A116: ( q in B & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
reconsider p9 = p as Element of A by A115;
per cases ( ( p in A & q = {A} & u = {A} ) or ( p in A & q = {A} & u = {{A}} ) or ( p in A & q = {A} & u = {{{A}}} ) or ( p in A & q = {{A}} & u = {A} ) or ( p in A & q = {{A}} & u = {{A}} ) or ( p in A & q = {{A}} & u = {{{A}}} ) or ( p in A & q = {{{A}}} & u = {A} ) or ( p in A & q = {{{A}}} & u = {{A}} ) or ( p in A & q = {{{A}}} & u = {{{A}}} ) ) by A115, A116, ENUMSET1:def 1;
suppose A117: ( p in A & q = {A} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,q)) by Def10
.= (new_bi_fun (d,q)) . (p,q) by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A117; :: thesis: verum
end;
suppose A118: ( p in A & q = {A} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then (new_bi_fun (d,q)) . (p,u) = ((d . (p9,(q `1_4))) "\/" a) "\/" b by Def10
.= ((new_bi_fun (d,q)) . (p,q)) "\/" b by A118, Def10 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A118, Def10; :: thesis: verum
end;
suppose A119: ( p in A & q = {A} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (p9,(q `2_4)) <= (d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4))) by A2;
then (d . (p9,(q `2_4))) "\/" b <= ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b by WAYBEL_1:2;
then A120: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b by A119, Def10;
(d . (p9,(q `1_4))) "\/" b <= (d . (p9,(q `1_4))) "\/" b ;
then ( ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b = ((d . (p9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) & ((d . (p9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) <= ((d . (p9,(q `1_4))) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
then A121: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `1_4))) "\/" b) "\/" (a "\/" b) by A120, ORDERS_2:3;
A122: ((d . (p9,(q `1_4))) "\/" b) "\/" (a "\/" b) = (d . (p9,(q `1_4))) "\/" ((b "\/" a) "\/" b) by LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" (a "\/" (b "\/" b)) by LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" (a "\/" b) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" ((a "\/" a) "\/" b) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= ((d . (p9,(q `1_4))) "\/" a) "\/" (a "\/" b) by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `1_4))) "\/" a by A119, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A119, A121, A122, Def10; :: thesis: verum
end;
suppose A123: ( p in A & q = {{A}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then (new_bi_fun (d,q)) . (p,q) = ((d . (p9,(q `1_4))) "\/" a) "\/" b by Def10
.= ((new_bi_fun (d,q)) . (p,u)) "\/" b by A123, Def10 ;
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (((new_bi_fun (d,q)) . (p,u)) "\/" b) "\/" b by A123, Def10
.= ((new_bi_fun (d,q)) . (p,u)) "\/" (b "\/" b) by LATTICE3:14
.= ((new_bi_fun (d,q)) . (p,u)) "\/" b by YELLOW_5:1 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by YELLOW_0:22; :: thesis: verum
end;
suppose A124: ( p in A & q = {{A}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,q)) by Def10
.= (new_bi_fun (d,q)) . (p,q) by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A124; :: thesis: verum
end;
suppose A125: ( p in A & q = {{A}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (p9,(q `2_4)) <= (d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4))) by A2;
then (d . (p9,(q `2_4))) "\/" b <= ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b by WAYBEL_1:2;
then A126: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b by A125, Def10;
(d . (p9,(q `1_4))) "\/" b <= (d . (p9,(q `1_4))) "\/" b ;
then ( ((d . (p9,(q `1_4))) "\/" (d . ((q `1_4),(q `2_4)))) "\/" b = ((d . (p9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) & ((d . (p9,(q `1_4))) "\/" b) "\/" (d . ((q `1_4),(q `2_4))) <= ((d . (p9,(q `1_4))) "\/" b) "\/" (a "\/" b) ) by A14, LATTICE3:14, YELLOW_3:3;
then A127: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `1_4))) "\/" b) "\/" (a "\/" b) by A126, ORDERS_2:3;
A128: ((d . (p9,(q `1_4))) "\/" b) "\/" (a "\/" b) = (d . (p9,(q `1_4))) "\/" ((b "\/" a) "\/" b) by LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" (a "\/" (b "\/" b)) by LATTICE3:14
.= (d . (p9,(q `1_4))) "\/" (a "\/" b) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" ((a "\/" a) "\/" b) by YELLOW_5:1
.= (d . (p9,(q `1_4))) "\/" (a "\/" (a "\/" b)) by LATTICE3:14
.= ((d . (p9,(q `1_4))) "\/" (a "\/" b)) "\/" a by LATTICE3:14
.= (((d . (p9,(q `1_4))) "\/" a) "\/" b) "\/" a by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,q) = ((d . (p9,(q `1_4))) "\/" a) "\/" b by A125, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A125, A127, A128, Def10; :: thesis: verum
end;
suppose A129: ( p in A & q = {{{A}}} & u = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (p9,(q `1_4)) <= (d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4))) by A2;
then (d . (p9,(q `1_4))) "\/" a <= ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" a by WAYBEL_1:2;
then A130: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" a by A129, Def10;
( d . ((q `2_4),(q `1_4)) <= a "\/" b & (d . (p9,(q `2_4))) "\/" a <= (d . (p9,(q `2_4))) "\/" a ) by A1, A14;
then ( ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" a = ((d . (p9,(q `2_4))) "\/" a) "\/" (d . ((q `2_4),(q `1_4))) & ((d . (p9,(q `2_4))) "\/" a) "\/" (d . ((q `2_4),(q `1_4))) <= ((d . (p9,(q `2_4))) "\/" a) "\/" (a "\/" b) ) by LATTICE3:14, YELLOW_3:3;
then A131: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `2_4))) "\/" a) "\/" (a "\/" b) by A130, ORDERS_2:3;
A132: ((d . (p9,(q `2_4))) "\/" a) "\/" (a "\/" b) = (((d . (p9,(q `2_4))) "\/" a) "\/" a) "\/" b by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" (a "\/" a)) "\/" b by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" a) "\/" b by YELLOW_5:1
.= (d . (p9,(q `2_4))) "\/" (a "\/" b) by LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" (a "\/" (b "\/" b)) by YELLOW_5:1
.= (d . (p9,(q `2_4))) "\/" ((a "\/" b) "\/" b) by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" b) "\/" (a "\/" b) by LATTICE3:14 ;
(new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" b by A129, Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A129, A131, A132, Def10; :: thesis: verum
end;
suppose A133: ( p in A & q = {{{A}}} & u = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
d . (p9,(q `1_4)) <= (d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4))) by A2;
then A134: (d . (p9,(q `1_4))) "\/" (a "\/" b) <= ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" (a "\/" b) by WAYBEL_1:2;
(new_bi_fun (d,q)) . (p,u) = ((d . (p9,(q `1_4))) "\/" a) "\/" b by A133, Def10;
then A135: (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" (a "\/" b) by A134, LATTICE3:14;
A136: ((d . (p9,(q `2_4))) "\/" a) "\/" (a "\/" b) = (((d . (p9,(q `2_4))) "\/" a) "\/" a) "\/" b by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" (a "\/" a)) "\/" b by LATTICE3:14
.= ((d . (p9,(q `2_4))) "\/" a) "\/" b by YELLOW_5:1
.= ((d . (p9,(q `2_4))) "\/" b) "\/" a by LATTICE3:14 ;
A137: (new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" b by A133, Def10;
A138: (d . (p9,(q `2_4))) "\/" (a "\/" b) <= (d . (p9,(q `2_4))) "\/" (a "\/" b) ;
( d . ((q `2_4),(q `1_4)) <= a "\/" b & ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" (a "\/" b) = ((d . (p9,(q `2_4))) "\/" (a "\/" b)) "\/" (d . ((q `2_4),(q `1_4))) ) by A1, A14, LATTICE3:14;
then A139: ((d . (p9,(q `2_4))) "\/" (d . ((q `2_4),(q `1_4)))) "\/" (a "\/" b) <= ((d . (p9,(q `2_4))) "\/" (a "\/" b)) "\/" (a "\/" b) by A138, YELLOW_3:3;
((d . (p9,(q `2_4))) "\/" a) "\/" (a "\/" b) = ((d . (p9,(q `2_4))) "\/" a) "\/" ((a "\/" b) "\/" (a "\/" b)) by YELLOW_5:1
.= (d . (p9,(q `2_4))) "\/" (a "\/" ((a "\/" b) "\/" (a "\/" b))) by LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" ((a "\/" (a "\/" b)) "\/" (a "\/" b)) by LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" (((a "\/" a) "\/" b) "\/" (a "\/" b)) by LATTICE3:14
.= (d . (p9,(q `2_4))) "\/" ((a "\/" b) "\/" (a "\/" b)) by YELLOW_5:1
.= ((d . (p9,(q `2_4))) "\/" (a "\/" b)) "\/" (a "\/" b) by LATTICE3:14 ;
then (new_bi_fun (d,q)) . (p,u) <= ((d . (p9,(q `2_4))) "\/" a) "\/" (a "\/" b) by A139, A135, ORDERS_2:3;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A133, A137, A136, Def10; :: thesis: verum
end;
suppose A140: ( p in A & q = {{{A}}} & u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) = (Bottom L) "\/" ((new_bi_fun (d,q)) . (p,q)) by Def10
.= (new_bi_fun (d,q)) . (p,q) by WAYBEL_1:3 ;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A140; :: thesis: verum
end;
end;
end;
A141: for p, q, u being Element of new_set A st p in A & q in A & u in A holds
(new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: ( p in A & q in A & u in A implies (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) )
assume ( p in A & q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
then reconsider p9 = p, q9 = q, u9 = u as Element of A ;
A142: (new_bi_fun (d,q)) . (q,u) = d . (q9,u9) by Def10;
( (new_bi_fun (d,q)) . (p,u) = d . (p9,u9) & (new_bi_fun (d,q)) . (p,q) = d . (p9,q9) ) by Def10;
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A2, A142; :: thesis: verum
end;
for p, q, u being Element of new_set A holds (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
proof
let p, q, u be Element of new_set A; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
per cases ( ( p in A & q in A & u in A ) or ( p in A & q in A & u in B ) or ( p in A & q in B & u in A ) or ( p in A & q in B & u in B ) or ( p in B & q in A & u in A ) or ( p in B & q in A & u in B ) or ( p in B & q in B & u in A ) or ( p in B & q in B & u in B ) ) by XBOOLE_0:def 3;
suppose ( p in A & q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A141; :: thesis: verum
end;
suppose ( p in A & q in A & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A54; :: thesis: verum
end;
suppose ( p in A & q in B & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A3; :: thesis: verum
end;
suppose ( p in A & q in B & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A114; :: thesis: verum
end;
suppose ( p in B & q in A & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A42; :: thesis: verum
end;
suppose ( p in B & q in A & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A98; :: thesis: verum
end;
suppose ( p in B & q in B & u in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A15; :: thesis: verum
end;
suppose ( p in B & q in B & u in B ) ; :: thesis: (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u))
hence (new_bi_fun (d,q)) . (p,u) <= ((new_bi_fun (d,q)) . (p,q)) "\/" ((new_bi_fun (d,q)) . (q,u)) by A65; :: thesis: verum
end;
end;
end;
hence new_bi_fun (d,q) is u.t.i. ; :: thesis: verum