let X be set ; :: thesis: InclPoset (Filt (BoolePoset X)) is upper-bounded
set L = InclPoset (Filt (BoolePoset X));
bool X is Filter of (BoolePoset X) by Th11;
then bool X in { Z where Z is Filter of (BoolePoset X) : verum } ;
then bool X in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def 24;
then reconsider x = bool X as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def 1;
now :: thesis: for b being Element of (InclPoset (Filt (BoolePoset X))) st b in the carrier of (InclPoset (Filt (BoolePoset X))) holds
b <= x
let b be Element of (InclPoset (Filt (BoolePoset X))); :: thesis: ( b in the carrier of (InclPoset (Filt (BoolePoset X))) implies b <= x )
assume b in the carrier of (InclPoset (Filt (BoolePoset X))) ; :: thesis: b <= x
then b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
then b in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def 24;
then ex b1 being Filter of (BoolePoset X) st b1 = b ;
then b c= the carrier of (BoolePoset X) ;
then b c= bool X by WAYBEL_7:2;
hence b <= x by YELLOW_1:3; :: thesis: verum
end;
then x is_>=_than the carrier of (InclPoset (Filt (BoolePoset X))) by LATTICE3:def 9;
hence InclPoset (Filt (BoolePoset X)) is upper-bounded by YELLOW_0:def 5; :: thesis: verum