let X be set ; :: thesis:
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 x = {X} as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def 1;

let b be Element of (InclPoset (Filt (BoolePoset X))); :: thesis:
assume b in the carrier of (InclPoset (Filt (BoolePoset X))) ; :: thesis:
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
A1: b1 = b ;
consider d being object such that
A2: d in b1 by XBOOLE_0:def 1;
reconsider d = d as set by TARSKI:1;
A3: d c= X by A2, WAYBEL_8:26;

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

end;

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

end;

then x is_<=_than the carrier of (InclPoset (Filt (BoolePoset X))) by LATTICE3:def 8;
hence InclPoset (Filt (BoolePoset X)) is lower-bounded by YELLOW_0:def 4; :: thesis: