let P, Q be non empty flat Poset; :: thesis: for f being Function of P,Q st f . (Bottom P) = Bottom Q holds
f is monotone
let f be Function of P,Q; :: thesis: ( f . (Bottom P) = Bottom Q implies f is monotone )
assume A1: f . (Bottom P) = Bottom Q ; :: thesis: f is monotone
set z = Bottom P;
for p1, p2 being Element of P st p1 <= p2 holds
for q1, q2 being Element of Q st q1 = f . p1 & q2 = f . p2 holds
q1 <= q2

proof

let p1, p2 be Element of P; :: thesis: ( p1 <= p2 implies for q1, q2 being Element of Q st q1 = f . p1 & q2 = f . p2 holds
q1 <= q2 )
assume p1 <= p2 ; :: thesis: for q1, q2 being Element of Q st q1 = f . p1 & q2 = f . p2 holds
q1 <= q2
then ( p1 = Bottom P or p1 = p2 ) by Lemflat01;
hence for q1, q2 being Element of Q st q1 = f . p1 & q2 = f . p2 holds
q1 <= q2 by A1, Lemflat01; :: thesis: verum

end;

hence f is monotone ; :: thesis: verum