let L be Lattice; :: thesis:
assume A1: ( L is distributive & L is finite ) ; :: thesis:
then reconsider L = L as D0_Lattice ;
set C = the carrier of L;
L is implicative

let p, q be Element of the carrier of L; :: according to FILTER_0:def 6 :: thesis:
defpred S₁[ Element of the carrier of L] means p "/\" c₁ [= q;
set B = { x where x is Element of the carrier of L : S₁[x] } ;
A2: { x where x is Element of the carrier of L : S₁[x] } c= the carrier of L from FRAENKEL:sch 10();
then { x where x is Element of the carrier of L : S₁[x] } is finite by A1, FINSET_1:1;
then reconsider B = { x where x is Element of the carrier of L : S₁[x] } as Element of Fin the carrier of L by A2, FINSUB_1:def 5;
take r = FinJoin (B,(id the carrier of L)); :: thesis:

let x be Element of the carrier of L; :: thesis:
assume x in B ; :: thesis:
then A4: ex x9 being Element of the carrier of L st
( x9 = x & p "/\" x9 [= q ) ;
( the L_meet of L [;] (p,(id the carrier of L))) . x = the L_meet of L . (p,((id the carrier of L) . x)) by FUNCOP_1:53
.= p "/\" x ;
hence ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q by A4; :: thesis:

end;

p "/\" r = FinJoin (B,( the L_meet of L [;] (p,(id the carrier of L)))) by Th64;
hence p "/\" r [= q by A3, Th54; :: thesis:
let r1 be Element of the carrier of L; :: thesis:
assume p "/\" r1 [= q ; :: thesis:
then A5: r1 in B ;
r1 = (id the carrier of L) . r1 ;
hence r1 [= r by A5, Th28; :: thesis:

end;