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 = { (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

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

( 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

q in AA

D c= AA

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

A32: c in { (FinMeet C) 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 { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A32, A33, LATTICES:8;

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

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 = { (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

not { a where a is Element of L : ex c being Element of L st
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 { (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;( 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

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

proof

then reconsider AA = { a where a is Element of L : ex c being Element of L st
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 { (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;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 { (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

( 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

for p, q being Element of L st p in AA & p [= q holds
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:23;

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;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:23;

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

q in AA

proof

then A28:
AA is Filter of L
by A7, FILTER_0:9;
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;

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:7;

hence q in AA ; :: thesis: verum

end;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;

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:7;

hence q in AA ; :: thesis: verum

D c= AA

proof

then
<.D.) c= AA
by A28, FILTER_0:def 4;
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 A29, ZFMISC_1:31;

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 A29, FUNCT_1:18

.= the L_meet of L $$ (C,(id the carrier of L)) by A29, SETWISEO:17

.= FinMeet (C,(id L)) by LATTICE2:def 4

.= FinMeet C by LATTICE4:def 9 ;

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 A31; :: thesis: verum

end;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 A29, ZFMISC_1:31;

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 A29, FUNCT_1:18

.= the L_meet of L $$ (C,(id the carrier of L)) by A29, SETWISEO:17

.= FinMeet (C,(id L)) by LATTICE2:def 4

.= FinMeet C by LATTICE4:def 9 ;

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 A31; :: thesis: verum

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

A32: c in { (FinMeet C) 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 { (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} ) } by A32, A33, LATTICES:8;

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