let X be set ; :: thesis: Top (InclPoset (Filt (BoolePoset X))) = bool X
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 bX = bool X as Element of by YELLOW_1:def 1;
A1: for b being Element of st b is_<=_than {} holds
bX >= b

proof

let b be Element of ; :: thesis: ( b is_<=_than {} implies bX >= b )
assume b is_<=_than {} ; :: thesis: bX >= b
b in the carrier of (InclPoset (Filt (BoolePoset 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:4;
hence bX >= b by YELLOW_1:3; :: thesis: verum

end;

bX is_<=_than {} by YELLOW_0:6;
then "/\" {} ,(InclPoset (Filt (BoolePoset X))) = bool X by A1, YELLOW_0:31;
hence Top (InclPoset (Filt (BoolePoset X))) = bool X by YELLOW_0:def 12; :: thesis: verum