let L be non trivial B_Lattice; :: thesis: for D being non empty Subset of L st Bottom L in <.D.) holds
ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L )
let D be non empty Subset of L; :: thesis: ( Bottom L in <.D.) implies ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L ) )
assume A1: Bottom L in <.D.) ; :: thesis: ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L )
set A = { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } ;
set AA = { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } ;
A2: { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } c= the carrier of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } or x in the carrier of L )
assume x in { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } ; :: thesis: x in the carrier of L
then consider a being Element of L such that
A3: ( a = x & ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) ) ;
thus x in the carrier of L by A3; :: thesis: verum

end;

not { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } is empty

proof

consider C being Finite_Subset of D such that
A4: not C is empty by Th32;
A5: C is Subset of D by FINSUB_1:32;
then C c= the carrier of L by XBOOLE_1:1;
then C is Element of Fin the carrier of L by FINSUB_1:def 5;
then consider C being Element of Fin the carrier of L such that
A6: ( C <> {} & C c= D ) by A4, A5;
reconsider a = FinMeet C as Element of L ;
a in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A6;
then consider c being Element of L such that
A7: ( c = a & c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) ;
a in { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } by A7;
hence not { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } is empty ; :: thesis: verum

end;

then reconsider AA = { a where a is Element of L : ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } as non empty Subset of L by A2;
A8: AA is Filter of L

proof

A9: for p, q being Element of L st p in AA & q in AA holds
p "/\" q in AA

proof

let p, q be Element of L; :: thesis: ( p in AA & q in AA implies p "/\" q in AA )
assume A10: ( p in AA & q in AA ) ; :: thesis: p "/\" q in AA
then consider a being Element of L such that
A11: ( a = p & ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) ) ;
consider c being Element of L such that
A12: ( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) by A11;
consider b being Element of L such that
A13: ( b = q & ex d being Element of L st
( d in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & d [= b ) ) by A10;
consider d being Element of L such that
A14: ( d in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & d [= b ) by A13;
A15: c "/\" d [= a "/\" b by A12, A14, FILTER_0:5;
consider C being Element of Fin the carrier of L such that
A16: ( c = FinMeet C & C c= D & C <> {} ) by A12;
consider E being Element of Fin the carrier of L such that
A17: ( d = FinMeet E & E c= D & E <> {} ) by A14;
A18: c "/\" d = FinMeet (C \/ E) by A16, A17, LATTICE4:30;
( C \/ E c= D & C \/ E <> {} ) by A16, A17, XBOOLE_1:8;
then c "/\" d in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A18;
hence p "/\" q in AA by A11, A13, A15; :: thesis: verum

end;

for p, q being Element of L st p in AA & p [= q holds
q in AA

proof

let p, q be Element of L; :: thesis: ( p in AA & p [= q implies q in AA )
assume A19: ( p in AA & p [= q ) ; :: thesis: q in AA
then consider a being Element of L such that
A20: ( a = p & ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) ) ;
consider c being Element of L;
consider b being Element of L such that
A21: ( b = q & ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= b ) ) by A19, A20, LATTICES:25;
thus q in AA by A21; :: thesis: verum

end;

hence AA is Filter of L by A9, FILTER_0:9; :: thesis: verum

end;

D c= AA

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in AA )
assume A22: x in D ; :: thesis: x in AA
then A23: ( {x} c= D & {x} <> {} ) by ZFMISC_1:37;
{x} c= the carrier of L by A22, ZFMISC_1:37;
then reconsider C = {x} as Element of Fin the carrier of L by FINSUB_1:def 5;
A24: ( the L_meet of L is commutative & the L_meet of L is associative ) by LATTICE2:31, LATTICE2:32;
A25: x = (id the carrier of L) . x by A22, FUNCT_1:35
.= the L_meet of L $$ C,(id the carrier of L) by A22, A24, SETWISEO:26
.= FinMeet C,(id L) by LATTICE2:def 4
.= FinMeet C by LATTICE4:def 13 ;
reconsider a = FinMeet C as Element of L ;
( a in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & a [= a ) by A23;
hence x in AA by A25; :: thesis: verum

end;

then <.D.) c= AA by A8, FILTER_0:def 5;
then Bottom L in AA by A1;
then ex d being Element of L st
( d = Bottom L & ex c being Element of L st
( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= d ) ) ;
then consider c being Element of L such that
A26: ( c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= Bottom L ) ;
Bottom L [= c by LATTICES:41;
then Bottom L in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A26, LATTICES:26;
then ex C being Finite_Subset of the carrier of L st
( Bottom L = FinMeet C & C c= D & C <> {} ) ;
hence ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L ) ; :: thesis: verum