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 and
s is monotone and
A2: for x being Element of L holds s . x c= downarrow x by Def13;
IdsMap L >= s
proof
let a be set ; :: according to YELLOW_2:def 1 :: thesis: ( not a in the carrier of L or ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . a & b2 = (IdsMap L) . a & b1 <= b2 ) )
assume a in the carrier of L ; :: thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . a & b2 = (IdsMap L) . a & b1 <= b2 )
then reconsider a9 = a as Element of L ;
A3: (IdsMap L) . a = downarrow a9 by YELLOW_2:def 4;
A4: s . a c= downarrow a9 by A2;
reconsider A = s . a9, B = (IdsMap L) . a9 as Element of (InclPoset (Ids L)) ;
take A ; :: thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( A = s . a & b1 = (IdsMap L) . a & A <= b1 )
take B ; :: thesis: ( A = s . a & B = (IdsMap L) . a & A <= B )
thus ( A = s . a & B = (IdsMap L) . a & A <= B ) by A3, A4, YELLOW_1:3; :: thesis: verum
end;
then [b,x] in the InternalRel of (MonSet L) by A1, Def13;
hence b <= x by ORDERS_2:def 5; :: thesis: verum
end;
hence ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L) ; :: thesis: verum