let P, Q be non empty strict chain-complete Poset; :: thesis: for f being Function of P,Q holds f <= f
let f be Function of P,Q; :: thesis: f <= f
for p being Element of P holds f . p <= f . p ;
hence f <= f by YELLOW_2:9; :: thesis: verum