let P, Q be non empty strict chain-complete Poset; :: thesis: for f, g, h being Function of P,Q st f <= g & g <= h holds
f <= h
let f, g, h be Function of P,Q; :: thesis: ( f <= g & g <= h implies f <= h )
assume A1: ( f <= g & g <= h ) ; :: thesis: f <= h
for p being Element of P holds f . p <= h . p

proof

let p be Element of P; :: thesis: f . p <= h . p
for q, q2 being Element of Q st q = f . p & q2 = h . p holds
q <= q2

proof

let q, q2 be Element of Q; :: thesis: ( q = f . p & q2 = h . p implies q <= q2 )
assume A2: ( q = f . p & q2 = h . p ) ; :: thesis: q <= q2
set q1 = g . p;
( q <= g . p & g . p <= q2 ) by A2, A1, YELLOW_2:9;
hence q <= q2 by ORDERS_2:3; :: thesis: verum

end;

hence f . p <= h . p ; :: thesis: verum

end;

hence f <= h by YELLOW_2:9; :: thesis: verum