let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)
let AR be auxiliary Relation of L; :: thesis: [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)
set c = the carrier of L --> {(Bottom L)};
set d = AR -below ;
ex f, g being Function of L,(InclPoset (Ids L)) st
( the carrier of L --> {(Bottom L)} = f & AR -below = g & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & f <= g )
proof
reconsider c = the carrier of L --> {(Bottom L)} as Function of L,(InclPoset (Ids L)) by Th25;
take c ; :: thesis: ex g being Function of L,(InclPoset (Ids L)) st
( the carrier of L --> {(Bottom L)} = c & AR -below = g & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & c <= g )
take AR -below ; :: thesis: ( the carrier of L --> {(Bottom L)} = c & AR -below = AR -below & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & c <= AR -below )
c <= AR -below
proof
let x be set ; :: according to YELLOW_2:def 1 :: thesis: ( not x in the carrier of L or ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = c . x & b2 = (AR -below) . x & b1 <= b2 ) )
assume x in the carrier of L ; :: thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = c . x & b2 = (AR -below) . x & b1 <= b2 )
then reconsider x9 = x as Element of L ;
(AR -below) . x = AR -below x9 by Def12;
then reconsider dx = (AR -below) . x9 as Ideal of L ;
reconsider dx9 = dx as Element of (InclPoset (Ids L)) ;
A1: c . x c= dx by Lm4;
take c . x9 ; :: thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( c . x9 = c . x & b1 = (AR -below) . x & c . x9 <= b1 )
take dx9 ; :: thesis: ( c . x9 = c . x & dx9 = (AR -below) . x & c . x9 <= dx9 )
thus ( c . x9 = c . x & dx9 = (AR -below) . x & c . x9 <= dx9 ) by A1, YELLOW_1:3; :: thesis: verum
end;
hence ( the carrier of L --> {(Bottom L)} = c & AR -below = AR -below & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & c <= AR -below ) by Th18, Th26; :: thesis: verum
end;
hence [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L) by Def13; :: thesis: verum