let L be lower-bounded sup-Semilattice; :: thesis: for f being Function of L,(InclPoset (Ids L)) st f = the carrier of L --> {(Bottom L)} holds
f is monotone
let f be Function of L,(InclPoset (Ids L)); :: thesis: ( f = the carrier of L --> {(Bottom L)} implies f is monotone )
assume A1: f = the carrier of L --> {(Bottom L)} ; :: thesis: f is monotone
let x, y be Element of L; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) )
A2: f . x = {(Bottom L)} by A1, FUNCOP_1:7;
f . y = {(Bottom L)} by A1, FUNCOP_1:7;
hence ( not x <= y or for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) ) by A2, YELLOW_1:3; :: thesis: verum