let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary Relation of L holds AR -below in the carrier of (MonSet L)
let AR be auxiliary Relation of L; :: thesis: AR -below in the carrier of (MonSet L)
set s = AR -below ;
ex s being Function of L,(InclPoset (Ids L)) st
( AR -below = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) )

proof

take AR -below ; :: thesis: ( AR -below = AR -below & AR -below is monotone & ( for x being Element of L holds (AR -below) . x c= downarrow x ) )
for x being Element of L holds (AR -below) . x c= downarrow x

proof

let x be Element of L; :: thesis: (AR -below) . x c= downarrow x
(AR -below) . x = AR -below x by Def12;
hence (AR -below) . x c= downarrow x by Th12; :: thesis: verum

end;

hence ( AR -below = AR -below & AR -below is monotone & ( for x being Element of L holds (AR -below) . x c= downarrow x ) ) ; :: thesis: verum

end;

hence AR -below in the carrier of (MonSet L) by Def13; :: thesis: verum