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.
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;
assume A4: d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) ; :: thesis: new_bi_fun2 d,q is u.t.i.
reconsider B = {{A},{{A}}} as non empty set ;
reconsider a = q `3 , b = q `4 as Element of L ;
A5: 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 p' = p, q' = q, u' = u as Element of A ;
A6: (new_bi_fun2 d,q) . p,u = d . p',u' by Def5;
A7: (new_bi_fun2 d,q) . p,q = d . p',q' by Def5;
(new_bi_fun2 d,q) . q,u = d . q',u' 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, A6, A7, LATTICE5:def 8; :: thesis: verum

end;

A8: 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 A9: ( 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 A9, TARSKI:def 2;

suppose A10: ( 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 p' = p, q' = q as Element of A ;
A11: (new_bi_fun2 d,q) . p,u = (d . p',(q `1 )) "\/" a by A10, Def5;
A12: (new_bi_fun2 d,q) . q,u = (d . q',(q `1 )) "\/" a by A10, Def5;
A13: (new_bi_fun2 d,q) . p,q = d . p',q' by Def5;
d . p',(q `1 ) <= (d . p',q') "\/" (d . q',(q `1 )) by A3, LATTICE5:def 8;
then (d . p',(q `1 )) "\/" a <= ((d . p',q') "\/" (d . q',(q `1 ))) "\/" a 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 A11, A12, A13, LATTICE3:14; :: thesis: verum

end;

suppose A14: ( 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 p' = p, q' = q as Element of A ;
A15: (new_bi_fun2 d,q) . p,u = (d . p',(q `2 )) "\/" a by A14, Def5;
A16: (new_bi_fun2 d,q) . q,u = (d . q',(q `2 )) "\/" a by A14, Def5;
A17: (new_bi_fun2 d,q) . p,q = d . p',q' by Def5;
d . p',(q `2 ) <= (d . p',q') "\/" (d . q',(q `2 )) by A3, LATTICE5:def 8;
then (d . p',(q `2 )) "\/" a <= ((d . p',q') "\/" (d . q',(q `2 ))) "\/" a 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, A16, A17, LATTICE3:14; :: thesis: verum

end;

end;

end;

A18: 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 A19: ( 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 A19, TARSKI:def 2;

suppose A20: ( 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 p' = p, u' = u as Element of A ;
A21: (new_bi_fun2 d,q) . p,q = (d . p',(q `1 )) "\/" a by A20, Def5;
A22: (new_bi_fun2 d,q) . q,u = (d . u',(q `1 )) "\/" a by A20, Def5;
A23: (d . p',(q `1 )) "\/" (d . u',(q `1 )) <= ((d . p',(q `1 )) "\/" (d . u',(q `1 ))) "\/" a by YELLOW_0:22;
A24: ((d . p',(q `1 )) "\/" (d . u',(q `1 ))) "\/" a = (d . p',(q `1 )) "\/" ((d . u',(q `1 )) "\/" a) by LATTICE3:14
.= (d . p',(q `1 )) "\/" ((d . u',(q `1 )) "\/" (a "\/" a)) by YELLOW_5:1
.= (d . p',(q `1 )) "\/" (((d . u',(q `1 )) "\/" a) "\/" a) by LATTICE3:14
.= ((d . p',(q `1 )) "\/" a) "\/" ((d . u',(q `1 )) "\/" a) by LATTICE3:14 ;
d . p',u' <= (d . p',(q `1 )) "\/" (d . (q `1 ),u') by A3, LATTICE5:def 8;
then d . p',u' <= (d . p',(q `1 )) "\/" (d . u',(q `1 )) by A2, LATTICE5:def 6;
then d . p',u' <= ((d . p',(q `1 )) "\/" a) "\/" ((d . u',(q `1 )) "\/" a) by A23, A24, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A21, A22, Def5; :: thesis: verum

end;

suppose A25: ( 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 p' = p, u' = u as Element of A ;
A26: (new_bi_fun2 d,q) . p,q = (d . p',(q `2 )) "\/" a by A25, Def5;
A27: (new_bi_fun2 d,q) . q,u = (d . u',(q `2 )) "\/" a by A25, Def5;
A28: (d . p',(q `2 )) "\/" (d . u',(q `2 )) <= ((d . p',(q `2 )) "\/" (d . u',(q `2 ))) "\/" a by YELLOW_0:22;
A29: ((d . p',(q `2 )) "\/" (d . u',(q `2 ))) "\/" a = (d . p',(q `2 )) "\/" ((d . u',(q `2 )) "\/" a) by LATTICE3:14
.= (d . p',(q `2 )) "\/" ((d . u',(q `2 )) "\/" (a "\/" a)) by YELLOW_5:1
.= (d . p',(q `2 )) "\/" (((d . u',(q `2 )) "\/" a) "\/" a) by LATTICE3:14
.= ((d . p',(q `2 )) "\/" a) "\/" ((d . u',(q `2 )) "\/" a) by LATTICE3:14 ;
d . p',u' <= (d . p',(q `2 )) "\/" (d . (q `2 ),u') by A3, LATTICE5:def 8;
then d . p',u' <= (d . p',(q `2 )) "\/" (d . u',(q `2 )) by A2, LATTICE5:def 6;
then d . p',u' <= ((d . p',(q `2 )) "\/" a) "\/" ((d . u',(q `2 )) "\/" a) by A28, A29, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A26, A27, Def5; :: thesis: verum

end;

end;

end;

A30: 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 A31: ( 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 A31, TARSKI:def 2;

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

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

end;

suppose A33: ( 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 p' = p as Element of A ;
A34: (new_bi_fun2 d,q) . p,q = (d . p',(q `1 )) "\/" a by A33, Def5;
A35: (new_bi_fun2 d,q) . q,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A33, Def5;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A36: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
A37: (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) by YELLOW_5:2;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A4, 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 A38: (d . p',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . p',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by WAYBEL_1:3;
((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . p',(q `1 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A34, A35, A36, LATTICE3:14
.= (d . p',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . p',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then A39: ((d . p',(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A37, A38, LATTICE3:14;
d . p',(q `2 ) <= (d . p',(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then (d . p',(q `2 )) "\/" a <= ((d . p',(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
then (d . p',(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A39, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A33, Def5; :: thesis: verum

end;

suppose A40: ( 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 p' = p as Element of A ;
A41: (new_bi_fun2 d,q) . p,q = (d . p',(q `2 )) "\/" a by A40, Def5;
A42: (new_bi_fun2 d,q) . q,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A40, Def5;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A43: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
A44: (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) by YELLOW_5:2;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A4, 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 A45: (d . p',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . p',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by WAYBEL_1:3;
((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . p',(q `2 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A41, A42, A43, LATTICE3:14
.= (d . p',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . p',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then A46: ((d . p',(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A44, A45, LATTICE3:14;
d . (q `2 ),(q `1 ) = d . (q `1 ),(q `2 ) by A2, LATTICE5:def 6;
then d . p',(q `1 ) <= (d . p',(q `2 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then (d . p',(q `1 )) "\/" a <= ((d . p',(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
then (d . p',(q `1 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A46, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A40, Def5; :: thesis: verum

end;

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

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

end;

end;

end;

A48: 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 A49: ( 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)
then reconsider q' = q, u' = u as Element of A ;

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

suppose A50: ( 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)

then A51: (new_bi_fun2 d,q) . p,q = (d . q',(q `1 )) "\/" a by Def5;
A52: (new_bi_fun2 d,q) . q,u = d . q',u' by Def5;
d . u',(q `1 ) <= (d . u',q') "\/" (d . q',(q `1 )) by A3, LATTICE5:def 8;
then d . u',(q `1 ) <= (d . q',u') "\/" (d . q',(q `1 )) by A2, LATTICE5:def 6;
then (d . u',(q `1 )) "\/" a <= ((d . q',(q `1 )) "\/" (d . q',u')) "\/" a by WAYBEL_1:3;
then (d . u',(q `1 )) "\/" a <= ((d . q',(q `1 )) "\/" a) "\/" (d . q',u') by LATTICE3:14;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A50, A51, A52, Def5; :: thesis: verum

end;

suppose A53: ( 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)

then A54: (new_bi_fun2 d,q) . p,q = (d . q',(q `2 )) "\/" a by Def5;
A55: (new_bi_fun2 d,q) . q,u = d . q',u' by Def5;
d . u',(q `2 ) <= (d . u',q') "\/" (d . q',(q `2 )) by A3, LATTICE5:def 8;
then d . u',(q `2 ) <= (d . q',u') "\/" (d . q',(q `2 )) by A2, LATTICE5:def 6;
then (d . u',(q `2 )) "\/" a <= ((d . q',(q `2 )) "\/" (d . q',u')) "\/" a by WAYBEL_1:3;
then (d . u',(q `2 )) "\/" a <= ((d . q',(q `2 )) "\/" a) "\/" (d . q',u') by LATTICE3:14;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A53, A54, A55, Def5; :: thesis: verum

end;

end;

end;

A56: 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 A57: ( 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 A57, 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 A58: ( 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 q' = q as Element of A ;
A59: (new_bi_fun2 d,q) . p,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A58, Def5;
(new_bi_fun2 d,q) . p,q = (d . q',(q `1 )) "\/" a by A58, Def5;
then A60: ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = ((d . q',(q `1 )) "\/" a) "\/" ((d . q',(q `2 )) "\/" a) by A58, Def5
.= ((d . q',(q `1 )) "\/" ((d . q',(q `2 )) "\/" a)) "\/" a by LATTICE3:14
.= (((d . q',(q `1 )) "\/" (d . q',(q `2 ))) "\/" a) "\/" a by LATTICE3:14
.= ((d . q',(q `1 )) "\/" (d . q',(q `2 ))) "\/" (a "\/" a) by LATTICE3:14
.= ((d . q',(q `1 )) "\/" (d . q',(q `2 ))) "\/" a by YELLOW_5:1 ;
d . q',(q `1 ) = d . (q `1 ),q' by A2, LATTICE5:def 6;
then d . (q `1 ),(q `2 ) <= (d . q',(q `1 )) "\/" (d . q',(q `2 )) by A3, LATTICE5:def 8;
then A61: (d . (q `1 ),(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A60, YELLOW_5:7;
((d . (q `1 ),(q `2 )) "\/" a) "/\" b <= (d . (q `1 ),(q `2 )) "\/" a by YELLOW_0:23;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A59, A61, ORDERS_2:26; :: thesis: verum

end;

suppose A62: ( 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 q' = q as Element of A ;
A63: (new_bi_fun2 d,q) . p,u = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A62, Def5;
(new_bi_fun2 d,q) . p,q = (d . q',(q `2 )) "\/" a by A62, Def5;
then A64: ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = ((d . q',(q `1 )) "\/" a) "\/" ((d . q',(q `2 )) "\/" a) by A62, Def5
.= ((d . q',(q `1 )) "\/" ((d . q',(q `2 )) "\/" a)) "\/" a by LATTICE3:14
.= (((d . q',(q `1 )) "\/" (d . q',(q `2 ))) "\/" a) "\/" a by LATTICE3:14
.= ((d . q',(q `1 )) "\/" (d . q',(q `2 ))) "\/" (a "\/" a) by LATTICE3:14
.= ((d . q',(q `1 )) "\/" (d . q',(q `2 ))) "\/" a by YELLOW_5:1 ;
d . q',(q `1 ) = d . (q `1 ),q' by A2, LATTICE5:def 6;
then d . (q `1 ),(q `2 ) <= (d . q',(q `1 )) "\/" (d . q',(q `2 )) by A3, LATTICE5:def 8;
then A65: (d . (q `1 ),(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A64, YELLOW_5:7;
((d . (q `1 ),(q `2 )) "\/" a) "/\" b <= (d . (q `1 ),(q `2 )) "\/" a by YELLOW_0:23;
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, ORDERS_2:26; :: thesis: verum

end;

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

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

end;

end;

end;

A66: 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 A67: ( 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 A67, TARSKI:def 2;

suppose A68: ( 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 A68, WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) ; :: thesis: verum

end;

suppose A69: ( 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 u' = u as Element of A ;
A70: (new_bi_fun2 d,q) . p,q = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A69, Def5;
A71: (new_bi_fun2 d,q) . q,u = (d . u',(q `1 )) "\/" a by A69, Def5;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A72: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
A73: (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) by YELLOW_5:2;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A4, 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 A74: (d . u',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . u',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by WAYBEL_1:3;
((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . u',(q `1 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A70, A71, A72, LATTICE3:14
.= (d . u',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . u',(q `1 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then A75: ((d . u',(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A73, A74, LATTICE3:14;
d . u',(q `2 ) <= (d . u',(q `1 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then (d . u',(q `2 )) "\/" a <= ((d . u',(q `1 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
then (d . u',(q `2 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A75, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A69, Def5; :: thesis: verum

end;

suppose A76: ( 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 u' = u as Element of A ;
A77: (new_bi_fun2 d,q) . p,q = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by A76, Def5;
A78: (new_bi_fun2 d,q) . q,u = (d . u',(q `2 )) "\/" a by A76, Def5;
a <= a "\/" (d . (q `1 ),(q `2 )) by YELLOW_0:22;
then A79: a "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" b) = (a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 ))) by A1, YELLOW11:def 3;
A80: (d . (q `1 ),(q `2 )) "\/" a = ((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a) by YELLOW_5:2;
a <= a ;
then (d . (q `1 ),(q `2 )) "\/" a <= (a "\/" b) "\/" a by A4, 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 A81: (d . u',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((d . (q `1 ),(q `2 )) "\/" a)) <= (d . u',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by WAYBEL_1:3;
((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) = (d . u',(q `2 )) "\/" ((a "\/" b) "/\" (a "\/" (d . (q `1 ),(q `2 )))) by A77, A78, A79, LATTICE3:14
.= (d . u',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" a) "\/" b)) by YELLOW_5:1
.= (d . u',(q `2 )) "\/" (((d . (q `1 ),(q `2 )) "\/" a) "/\" ((a "\/" b) "\/" a)) by LATTICE3:14 ;
then A82: ((d . u',(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A80, A81, LATTICE3:14;
d . (q `2 ),(q `1 ) = d . (q `1 ),(q `2 ) by A2, LATTICE5:def 6;
then d . u',(q `1 ) <= (d . u',(q `2 )) "\/" (d . (q `1 ),(q `2 )) by A3, LATTICE5:def 8;
then (d . u',(q `1 )) "\/" a <= ((d . u',(q `2 )) "\/" (d . (q `1 ),(q `2 ))) "\/" a by YELLOW_5:7;
then (d . u',(q `1 )) "\/" a <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A82, ORDERS_2:26;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A76, Def5; :: thesis: verum

end;

suppose A83: ( 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 A83, WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) ; :: thesis: verum

end;

end;

end;

A84: 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 A85: ( 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 A85, TARSKI:def 2;

suppose A86: ( 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 A86, Def5; :: thesis: verum

end;

suppose A87: ( 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 A87, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A87, Def5; :: thesis: verum

end;

suppose A88: ( 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 A88, Def5; :: thesis: verum

end;

suppose A89: ( 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 A89, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A89, Def5; :: thesis: verum

end;

suppose A90: ( 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 A90, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4
.= (new_bi_fun2 d,q) . p,q by A90, Def5 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A90; :: thesis: verum

end;

suppose A91: ( 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 A91, Def5; :: thesis: verum

end;

suppose A92: ( 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 A92, Def5
.= ((d . (q `1 ),(q `2 )) "\/" a) "/\" b by WAYBEL_1:4 ;
hence (new_bi_fun2 d,q) . p,u <= ((new_bi_fun2 d,q) . p,q) "\/" ((new_bi_fun2 d,q) . q,u) by A92, Def5; :: thesis: verum

end;

suppose A93: ( 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 A93, Def5; :: thesis: verum

end;

end;

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 A5; :: 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 A8; :: 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 A18; :: 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 A30; :: 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 A48; :: 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 A56; :: 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 A66; :: 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 A84; :: thesis: verum

end;

end;

end;

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