let X be set ; :: thesis: InclPoset (Filt (BoolePoset X)) is lower-bounded
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;

now

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

now

let c be set ; :: 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 A1, A2, A3, WAYBEL_7:7; :: thesis: verum

end;

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

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: verum