let X be set ; :: thesis: for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)
set L = BoolePoset X;
let Y be non empty Subset of (InclPoset (Filt (BoolePoset X))); :: thesis: meet Y is Filter of (BoolePoset X)

A1: now

let Z be set ; :: thesis: ( Z in Y implies Top (BoolePoset X) in Z )
assume Z in Y ; :: thesis: Top (BoolePoset X) in Z
then Z in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then Z in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
then Z in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then consider Z1 being Filter of (BoolePoset X) such that
A2: Z1 = Z ;
thus Top (BoolePoset X) in Z by A2, WAYBEL_4:22; :: thesis: verum

end;

Y c= the carrier of (InclPoset (Filt (BoolePoset X))) ;
then A3: Y c= the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
A4: Y c= bool the carrier of (BoolePoset X)

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in Y or v in bool the carrier of (BoolePoset X) )
assume v in Y ; :: thesis: v in bool the carrier of (BoolePoset X)
then v in Filt (BoolePoset X) by A3;
then v in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then consider v1 being Filter of (BoolePoset X) such that
A5: v1 = v ;
thus v in bool the carrier of (BoolePoset X) by A5; :: thesis: verum

end;

A6: for Z being Subset of (BoolePoset X) st Z in Y holds
Z is upper

proof

let Z be Subset of (BoolePoset X); :: thesis: ( Z in Y implies Z is upper )
assume Z in Y ; :: thesis: Z is upper
then Z in Filt (BoolePoset X) by A3;
then Z in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then consider Z1 being Filter of (BoolePoset X) such that
A7: Z1 = Z ;
thus Z is upper by A7; :: thesis: verum

end;

now

let V be Subset of (BoolePoset X); :: thesis: ( V in Y implies ( V is upper & V is filtered ) )
assume V in Y ; :: thesis: ( V is upper & V is filtered )
then V in Filt (BoolePoset X) by A3;
then V in { Z where Z is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then consider V1 being Filter of (BoolePoset X) such that
A8: V1 = V ;
thus V is upper by A8; :: thesis: V is filtered
thus V is filtered by A8; :: thesis: verum

end;

hence meet Y is Filter of (BoolePoset X) by A1, A4, A6, SETFAM_1:def 1, YELLOW_2:39, YELLOW_2:41; :: thesis: verum