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