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 :: thesis: for Z being set st Z in Y holds
Top (BoolePoset X) in Z
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 ex Z1 being Filter of (BoolePoset X) st Z1 = Z ;
hence Top (BoolePoset X) in Z by WAYBEL_4:22; :: thesis: verum
end;
Y c= the carrier of (InclPoset (Filt (BoolePoset X))) ;
then A2: Y c= the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
A3: 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 A2;
then Z in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then ex Z1 being Filter of (BoolePoset X) st Z1 = Z ;
hence Z is upper ; :: thesis: verum
end;
A4: now :: thesis: for V being Subset of (BoolePoset X) st V in Y holds
( V is upper & V is filtered )
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 A2;
then V in { Z where Z is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then A5: ex V1 being Filter of (BoolePoset X) st V1 = V ;
hence V is upper ; :: thesis: V is filtered
thus V is filtered by A5; :: thesis: verum
end;
Y c= bool the carrier of (BoolePoset X)
proof
let v be object ; :: 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 A2;
then v in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then ex v1 being Filter of (BoolePoset X) st v1 = v ;
hence v in bool the carrier of (BoolePoset X) ; :: thesis: verum
end;
hence meet Y is Filter of (BoolePoset X) by A1, A3, A4, SETFAM_1:def 1, YELLOW_2:37, YELLOW_2:39; :: thesis: verum