let X be set ; :: thesis: Bottom (InclPoset (Filt (BoolePoset X))) = {X}
set L = InclPoset (Filt (BoolePoset X));
{X} is Filter of (BoolePoset X) by Th12;
then {X} in { Z where Z is Filter of (BoolePoset X) : verum } ;
then {X} in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def 24;
then reconsider bX = {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 consider b1 being Filter of (BoolePoset X) such that
A2: b1 = b ;
consider d being object such that
A3: d in b1 by XBOOLE_0:def 1;
reconsider d = d as set by TARSKI:1;
A4: d c= X by A3, WAYBEL_8:26;

now :: thesis: for c being object st c in {X} holds
c in b

let c be object ; :: thesis: ( c in {X} implies c in b )
assume c in {X} ; :: thesis: c in b
then c = X by TARSKI:def 1;
hence c in b by A2, A3, A4, WAYBEL_7:7; :: thesis: verum

end;

then {X} c= b ;
hence bX <= b by YELLOW_1:3; :: thesis: verum

end;

bX is_>=_than {} by YELLOW_0:6;
then "\/" ({},(InclPoset (Filt (BoolePoset X)))) = {X} by A1, YELLOW_0:30;
hence Bottom (InclPoset (Filt (BoolePoset X))) = {X} by YELLOW_0:def 11; :: thesis: verum