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 ex a being Element of L st
( 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 ) ) ;
hence x in the carrier of L ; :: 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
A3: not C is empty by Th32;
A4: 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
A5: C <> {} and
A6: C c= D by A3, A4;
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 A5, A6;
then 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 ) } ;
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;
A7: 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 that
A8: p in AA and
A9: q in AA ; :: thesis: p "/\" q in AA
consider a being Element of L such that
A10: a = p and
A11: 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 A8;
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 <> {} ) } and
A13: c [= a by A11;
consider b being Element of L such that
A14: b = q and
A15: 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 A9;
consider d being Element of L such that
A16: d in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } and
A17: d [= b by A15;
A18: c "/\" d [= a "/\" b by A13, A17, FILTER_0:5;
consider C being Element of Fin the carrier of L such that
A19: c = FinMeet C and
A20: C c= D and
A21: C <> {} by A12;
consider E being Element of Fin the carrier of L such that
A22: d = FinMeet E and
A23: E c= D and
E <> {} by A16;
A24: c "/\" d = FinMeet (C \/ E) by A19, A22, LATTICE4:30;
C \/ E c= D by A20, A23, XBOOLE_1:8;
then c "/\" d in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A21, A24;
hence p "/\" q in AA by A10, A14, A18; :: 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 that
A25: p in AA and
A26: p [= q ; :: thesis: q in AA
A27: ex a being Element of L st
( 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 ) ) by A25;
consider c being Element of L;
ex b being Element of L st
( 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 A26, A27, LATTICES:25;
hence q in AA ; :: thesis: verum

end;

then A28: AA is Filter of L by A7, FILTER_0:9;
D c= AA

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in AA )
assume A29: x in D ; :: thesis: x in AA
then A30: {x} c= D by ZFMISC_1:37;
{x} c= the carrier of L by A29, ZFMISC_1:37;
then reconsider C = {x} as Element of Fin the carrier of L by FINSUB_1:def 5;
A32: x = (id the carrier of L) . x by A29, FUNCT_1:35
.= the L_meet of L $$ C,(id the carrier of L) by A29, 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 <> {} ) } by A30;
hence x in AA by A32; :: thesis: verum

end;

then <.D.) c= AA by A28, 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
A33: c in { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } and
A34: 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 A33, A34, 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