let L be lower-bounded sup-Semilattice; :: thesis: ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L)
set x = IdsMap L;
reconsider x = IdsMap L as Element of (MonSet L) by Th19;
x is_>=_than the carrier of (MonSet L)

proof

let b be Element of (MonSet L); :: according to LATTICE3:def 9 :: thesis: ( not b in the carrier of (MonSet L) or b <= x )
assume b in the carrier of (MonSet L) ; :: thesis: b <= x
consider s being Function of L,(InclPoset (Ids L)) such that
A1: ( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by Def14;
IdsMap L >= s

proof

let a be set ; :: according to YELLOW_2:def 1 :: thesis: ( not a in the carrier of L or ex b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) st
( b₁ = s . a & b₂ = (IdsMap L) . a & b₁ <= b₂ ) )
assume a in the carrier of L ; :: thesis: ex b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) st
( b₁ = s . a & b₂ = (IdsMap L) . a & b₁ <= b₂ )
then reconsider a' = a as Element of L ;
A2: (IdsMap L) . a = downarrow a' by YELLOW_2:def 4;
A3: s . a c= downarrow a' by A1;
reconsider A = s . a', B = (IdsMap L) . a' as Element of (InclPoset (Ids L)) ;
take A ; :: thesis: ex b₁ being Element of the carrier of (InclPoset (Ids L)) st
( A = s . a & b₁ = (IdsMap L) . a & A <= b₁ )
take B ; :: thesis: ( A = s . a & B = (IdsMap L) . a & A <= B )
thus ( A = s . a & B = (IdsMap L) . a & A <= B ) by A2, A3, YELLOW_1:3; :: thesis: verum

end;

then [b,x] in the InternalRel of (MonSet L) by A1, Def14;
hence b <= x by ORDERS_2:def 9; :: thesis: verum

end;

hence ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L) ; :: thesis: verum