let X be set ; :: thesis: for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds
( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
set L = InclPoset (Filt (BoolePoset X));
let Y be non empty Subset of (InclPoset (Filt (BoolePoset X))); :: thesis: ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
meet Y is Filter of (BoolePoset X) by Th9;
then meet Y in { Z where Z is Filter of (BoolePoset X) : verum } ;
then meet Y in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def 24;
then reconsider a = meet Y as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def 1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_<=_than Y holds
b <= a
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); :: thesis: ( b is_<=_than Y implies b <= a )
assume A2: b is_<=_than Y ; :: thesis: b <= a
for x being set st x in Y holds
b c= x by YELLOW_1:3, A2, LATTICE3:def 8;
then b c= meet Y by SETFAM_1:5;
hence b <= a by YELLOW_1:3; :: thesis: verum
end;
for b being Element of (InclPoset (Filt (BoolePoset X))) st b in Y holds
a <= b by YELLOW_1:3, SETFAM_1:3;
then a is_<=_than Y by LATTICE3:def 8;
hence ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y ) by A1, YELLOW_0:31; :: thesis: verum