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 Element of Fin 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 Element of Fin the carrier of L st
( B c= D & FinMeet B = Bottom L ) )

assume A1: Bottom L in <.D.) ; :: thesis: ex B being non empty Element of Fin the carrier of L st
( B c= D & FinMeet B = Bottom L )

set A = { () 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 { () 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 { () 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 object ; :: 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 { () 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 { () 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 { () 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 { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) } is empty
proof
consider C being Element of Fin D such that
A3: not C is empty by Th27;
A4: C is Subset of D by FINSUB_1:16;
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 { () 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 { () 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 { () 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 { () 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 { () 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 { () 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 { () 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 { () 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 ;
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 ;
C \/ E c= D by ;
then c "/\" d in { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by ;
hence p "/\" q in AA by ; :: 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 { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= a ) ) by A25;
ex b being Element of L st
( b = q & ex c being Element of L st
( c in { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } & c [= b ) ) by ;
hence q in AA ; :: thesis: verum
end;
then A28: AA is Filter of L by ;
D c= AA
proof
let x be object ; :: 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:31;
{x} c= the carrier of L by ;
then reconsider C = {x} as Element of Fin the carrier of L by FINSUB_1:def 5;
A31: x = (id the carrier of L) . x by
.= the L_meet of L \$\$ (C,(id the carrier of L)) by
.= FinMeet (C,(id L)) by LATTICE2:def 4
.= FinMeet C by LATTICE4:def 9 ;
reconsider a = FinMeet C as Element of L ;
a in { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A30;
hence x in AA by A31; :: thesis: verum
end;
then <.D.) c= AA by ;
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 { () 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
A32: c in { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } and
A33: c [= Bottom L ;
Bottom L [= c ;
then Bottom L in { () where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by ;
then ex C being Element of Fin the carrier of L st
( Bottom L = FinMeet C & C c= D & C <> {} ) ;
hence ex B being non empty Element of Fin the carrier of L st
( B c= D & FinMeet B = Bottom L ) ; :: thesis: verum