let n, m be Nat; :: thesis: for P being non empty strict chain-complete Poset
for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
let P be non empty strict chain-complete Poset; :: thesis: for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
let p, p1, p3, p4 be Element of P; :: thesis: for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
let g be monotone Function of P,P; :: thesis: ( n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p implies p1 <= p4 )
assume A1: ( n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p ) ; :: thesis: p1 <= p4
then consider k being Nat such that
A2: m = n + k by NAT_1:10;
thus p1 <= p4 by A1, A2, Lm4; :: thesis: verum