let n, m be Nat; 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; 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; 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; ( 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 )
; p1 <= p4
then consider k being Nat such that
A2:
m = n + k
by NAT_1:10;
thus
p1 <= p4
by A1, A2, Lm4; verum