let P, Q be non empty flat Poset; :: thesis:
let f be Function of P,Q; :: thesis:
assume A1: f . (Bottom P) = Bottom Q ; :: thesis:
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

let p1, p2 be Element of P; :: thesis:
assume p1 <= p2 ; :: thesis:
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:

end;