let L1, L2 be Lattice; :: thesis: ( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )

thus ( L1 is implicative & L2 is implicative implies [:L1,L2:] is implicative ) :: thesis: ( [:L1,L2:] is implicative implies ( L1 is implicative & L2 is implicative ) )

( a "/\" c [= b & ( for d being Element of [:L1,L2:] st a "/\" d [= b holds

d [= c ) ) ; :: according to FILTER_0:def 6 :: thesis: ( L1 is implicative & L2 is implicative )

thus for p1, q1 being Element of L1 ex r1 being Element of L1 st

( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) ) :: according to FILTER_0:def 6 :: thesis: L2 is implicative

let p2 be Element of L2; :: according to FILTER_0:def 6 :: thesis: for b_{1} being Element of the carrier of L2 ex b_{2} being Element of the carrier of L2 st

( p2 "/\" b_{2} [= b_{1} & ( for b_{3} being Element of the carrier of L2 holds

( not p2 "/\" b_{3} [= b_{1} or b_{3} [= b_{2} ) ) )

let q2 be Element of L2; :: thesis: ex b_{1} being Element of the carrier of L2 st

( p2 "/\" b_{1} [= q2 & ( for b_{2} being Element of the carrier of L2 holds

( not p2 "/\" b_{2} [= q2 or b_{2} [= b_{1} ) ) )

consider c being Element of [:L1,L2:] such that

A18: [ the Element of L1,p2] "/\" c [= [ the Element of L1,q2] and

A19: for d being Element of [:L1,L2:] st [ the Element of L1,p2] "/\" d [= [ the Element of L1,q2] holds

d [= c by A12;

consider r1 being Element of L1, r2 being Element of L2 such that

A20: c = [r1,r2] by DOMAIN_1:1;

take r2 ; :: thesis: ( p2 "/\" r2 [= q2 & ( for b_{1} being Element of the carrier of L2 holds

( not p2 "/\" b_{1} [= q2 or b_{1} [= r2 ) ) )

A21: [ the Element of L1,p2] "/\" c = [( the Element of L1 "/\" r1),(p2 "/\" r2)] by A20, Th21;

hence p2 "/\" r2 [= q2 by A18, Th36; :: thesis: for b_{1} being Element of the carrier of L2 holds

( not p2 "/\" b_{1} [= q2 or b_{1} [= r2 )

let s2 be Element of L2; :: thesis: ( not p2 "/\" s2 [= q2 or s2 [= r2 )

assume A22: p2 "/\" s2 [= q2 ; :: thesis: s2 [= r2

the Element of L1 "/\" r1 [= the Element of L1 by A18, A21, Th36;

then [( the Element of L1 "/\" r1),(p2 "/\" s2)] [= [ the Element of L1,q2] by A22, Th36;

then [ the Element of L1,p2] "/\" [r1,s2] [= [ the Element of L1,q2] by Th21;

then [r1,s2] [= c by A19;

hence s2 [= r2 by A20, Th36; :: thesis: verum

thus ( L1 is implicative & L2 is implicative implies [:L1,L2:] is implicative ) :: thesis: ( [:L1,L2:] is implicative implies ( L1 is implicative & L2 is implicative ) )

proof

assume A12:
for a, b being Element of [:L1,L2:] ex c being Element of [:L1,L2:] st
assume A1:
for p1, q1 being Element of L1 ex r1 being Element of L1 st

( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) ) ; :: according to FILTER_0:def 6 :: thesis: ( not L2 is implicative or [:L1,L2:] is implicative )

assume A2: for p2, q2 being Element of L2 ex r2 being Element of L2 st

( p2 "/\" r2 [= q2 & ( for s2 being Element of L2 st p2 "/\" s2 [= q2 holds

s2 [= r2 ) ) ; :: according to FILTER_0:def 6 :: thesis: [:L1,L2:] is implicative

let a, b be Element of [:L1,L2:]; :: according to FILTER_0:def 6 :: thesis: ex b_{1} being Element of the carrier of [:L1,L2:] st

( a "/\" b_{1} [= b & ( for b_{2} being Element of the carrier of [:L1,L2:] holds

( not a "/\" b_{2} [= b or b_{2} [= b_{1} ) ) )

consider p1 being Element of L1, p2 being Element of L2 such that

A3: a = [p1,p2] by DOMAIN_1:1;

consider q1 being Element of L1, q2 being Element of L2 such that

A4: b = [q1,q2] by DOMAIN_1:1;

consider r2 being Element of L2 such that

A5: p2 "/\" r2 [= q2 and

A6: for s2 being Element of L2 st p2 "/\" s2 [= q2 holds

s2 [= r2 by A2;

consider r1 being Element of L1 such that

A7: p1 "/\" r1 [= q1 and

A8: for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 by A1;

take [r1,r2] ; :: thesis: ( a "/\" [r1,r2] [= b & ( for b_{1} being Element of the carrier of [:L1,L2:] holds

( not a "/\" b_{1} [= b or b_{1} [= [r1,r2] ) ) )

a "/\" [r1,r2] = [(p1 "/\" r1),(p2 "/\" r2)] by A3, Th21;

hence a "/\" [r1,r2] [= b by A4, A7, A5, Th36; :: thesis: for b_{1} being Element of the carrier of [:L1,L2:] holds

( not a "/\" b_{1} [= b or b_{1} [= [r1,r2] )

let d be Element of [:L1,L2:]; :: thesis: ( not a "/\" d [= b or d [= [r1,r2] )

consider s1 being Element of L1, s2 being Element of L2 such that

A9: d = [s1,s2] by DOMAIN_1:1;

assume a "/\" d [= b ; :: thesis: d [= [r1,r2]

then A10: [(p1 "/\" s1),(p2 "/\" s2)] [= b by A3, A9, Th21;

then p2 "/\" s2 [= q2 by A4, Th36;

then A11: s2 [= r2 by A6;

p1 "/\" s1 [= q1 by A4, A10, Th36;

then s1 [= r1 by A8;

hence d [= [r1,r2] by A9, A11, Th36; :: thesis: verum

end;( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) ) ; :: according to FILTER_0:def 6 :: thesis: ( not L2 is implicative or [:L1,L2:] is implicative )

assume A2: for p2, q2 being Element of L2 ex r2 being Element of L2 st

( p2 "/\" r2 [= q2 & ( for s2 being Element of L2 st p2 "/\" s2 [= q2 holds

s2 [= r2 ) ) ; :: according to FILTER_0:def 6 :: thesis: [:L1,L2:] is implicative

let a, b be Element of [:L1,L2:]; :: according to FILTER_0:def 6 :: thesis: ex b

( a "/\" b

( not a "/\" b

consider p1 being Element of L1, p2 being Element of L2 such that

A3: a = [p1,p2] by DOMAIN_1:1;

consider q1 being Element of L1, q2 being Element of L2 such that

A4: b = [q1,q2] by DOMAIN_1:1;

consider r2 being Element of L2 such that

A5: p2 "/\" r2 [= q2 and

A6: for s2 being Element of L2 st p2 "/\" s2 [= q2 holds

s2 [= r2 by A2;

consider r1 being Element of L1 such that

A7: p1 "/\" r1 [= q1 and

A8: for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 by A1;

take [r1,r2] ; :: thesis: ( a "/\" [r1,r2] [= b & ( for b

( not a "/\" b

a "/\" [r1,r2] = [(p1 "/\" r1),(p2 "/\" r2)] by A3, Th21;

hence a "/\" [r1,r2] [= b by A4, A7, A5, Th36; :: thesis: for b

( not a "/\" b

let d be Element of [:L1,L2:]; :: thesis: ( not a "/\" d [= b or d [= [r1,r2] )

consider s1 being Element of L1, s2 being Element of L2 such that

A9: d = [s1,s2] by DOMAIN_1:1;

assume a "/\" d [= b ; :: thesis: d [= [r1,r2]

then A10: [(p1 "/\" s1),(p2 "/\" s2)] [= b by A3, A9, Th21;

then p2 "/\" s2 [= q2 by A4, Th36;

then A11: s2 [= r2 by A6;

p1 "/\" s1 [= q1 by A4, A10, Th36;

then s1 [= r1 by A8;

hence d [= [r1,r2] by A9, A11, Th36; :: thesis: verum

( a "/\" c [= b & ( for d being Element of [:L1,L2:] st a "/\" d [= b holds

d [= c ) ) ; :: according to FILTER_0:def 6 :: thesis: ( L1 is implicative & L2 is implicative )

thus for p1, q1 being Element of L1 ex r1 being Element of L1 st

( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) ) :: according to FILTER_0:def 6 :: thesis: L2 is implicative

proof

set p1 = the Element of L1;
set p2 = the Element of L2;

let p1, q1 be Element of L1; :: thesis: ex r1 being Element of L1 st

( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) )

consider c being Element of [:L1,L2:] such that

A13: [p1, the Element of L2] "/\" c [= [q1, the Element of L2] and

A14: for d being Element of [:L1,L2:] st [p1, the Element of L2] "/\" d [= [q1, the Element of L2] holds

d [= c by A12;

consider r1 being Element of L1, r2 being Element of L2 such that

A15: c = [r1,r2] by DOMAIN_1:1;

take r1 ; :: thesis: ( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) )

A16: [p1, the Element of L2] "/\" c = [(p1 "/\" r1),( the Element of L2 "/\" r2)] by A15, Th21;

hence p1 "/\" r1 [= q1 by A13, Th36; :: thesis: for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1

let s1 be Element of L1; :: thesis: ( p1 "/\" s1 [= q1 implies s1 [= r1 )

assume A17: p1 "/\" s1 [= q1 ; :: thesis: s1 [= r1

the Element of L2 "/\" r2 [= the Element of L2 by A13, A16, Th36;

then [(p1 "/\" s1),( the Element of L2 "/\" r2)] [= [q1, the Element of L2] by A17, Th36;

then [p1, the Element of L2] "/\" [s1,r2] [= [q1, the Element of L2] by Th21;

then [s1,r2] [= c by A14;

hence s1 [= r1 by A15, Th36; :: thesis: verum

end;let p1, q1 be Element of L1; :: thesis: ex r1 being Element of L1 st

( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) )

consider c being Element of [:L1,L2:] such that

A13: [p1, the Element of L2] "/\" c [= [q1, the Element of L2] and

A14: for d being Element of [:L1,L2:] st [p1, the Element of L2] "/\" d [= [q1, the Element of L2] holds

d [= c by A12;

consider r1 being Element of L1, r2 being Element of L2 such that

A15: c = [r1,r2] by DOMAIN_1:1;

take r1 ; :: thesis: ( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1 ) )

A16: [p1, the Element of L2] "/\" c = [(p1 "/\" r1),( the Element of L2 "/\" r2)] by A15, Th21;

hence p1 "/\" r1 [= q1 by A13, Th36; :: thesis: for s1 being Element of L1 st p1 "/\" s1 [= q1 holds

s1 [= r1

let s1 be Element of L1; :: thesis: ( p1 "/\" s1 [= q1 implies s1 [= r1 )

assume A17: p1 "/\" s1 [= q1 ; :: thesis: s1 [= r1

the Element of L2 "/\" r2 [= the Element of L2 by A13, A16, Th36;

then [(p1 "/\" s1),( the Element of L2 "/\" r2)] [= [q1, the Element of L2] by A17, Th36;

then [p1, the Element of L2] "/\" [s1,r2] [= [q1, the Element of L2] by Th21;

then [s1,r2] [= c by A14;

hence s1 [= r1 by A15, Th36; :: thesis: verum

let p2 be Element of L2; :: according to FILTER_0:def 6 :: thesis: for b

( p2 "/\" b

( not p2 "/\" b

let q2 be Element of L2; :: thesis: ex b

( p2 "/\" b

( not p2 "/\" b

consider c being Element of [:L1,L2:] such that

A18: [ the Element of L1,p2] "/\" c [= [ the Element of L1,q2] and

A19: for d being Element of [:L1,L2:] st [ the Element of L1,p2] "/\" d [= [ the Element of L1,q2] holds

d [= c by A12;

consider r1 being Element of L1, r2 being Element of L2 such that

A20: c = [r1,r2] by DOMAIN_1:1;

take r2 ; :: thesis: ( p2 "/\" r2 [= q2 & ( for b

( not p2 "/\" b

A21: [ the Element of L1,p2] "/\" c = [( the Element of L1 "/\" r1),(p2 "/\" r2)] by A20, Th21;

hence p2 "/\" r2 [= q2 by A18, Th36; :: thesis: for b

( not p2 "/\" b

let s2 be Element of L2; :: thesis: ( not p2 "/\" s2 [= q2 or s2 [= r2 )

assume A22: p2 "/\" s2 [= q2 ; :: thesis: s2 [= r2

the Element of L1 "/\" r1 [= the Element of L1 by A18, A21, Th36;

then [( the Element of L1 "/\" r1),(p2 "/\" s2)] [= [ the Element of L1,q2] by A22, Th36;

then [ the Element of L1,p2] "/\" [r1,s2] [= [ the Element of L1,q2] by Th21;

then [r1,s2] [= c by A19;

hence s2 [= r2 by A20, Th36; :: thesis: verum