let n, k be Nat; :: thesis: for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + k)) . p holds
p1 <= p4
let P be non empty strict chain-complete Poset; :: thesis: for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + k)) . p holds
p1 <= p4
let p3, p, p1, p4 be Element of P; :: thesis: for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + k)) . p holds
p1 <= p4
let g be monotone Function of P,P; :: thesis: ( p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + k)) . p implies p1 <= p4 )
defpred S₁[ Nat] means for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + $1)) . p holds
p1 <= p4;
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + k)) . p holds
p1 <= p4 ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let p, p3, p1, p4 be Element of P; :: thesis: ( p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + (k + 1))) . p implies p1 <= p4 )
assume B1: ( p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + (k + 1))) . p ) ; :: thesis: p1 <= p4
reconsider y1 = (iter g,(n + k)) . p as Element of P by Lemiter11;
B2: p1 <= y1 by B1, A3;
iter g,(n + (k + 1)) = iter g,((n + k) + 1)
.= (iter g,(n + k)) * g by FUNCT_7:71 ;
then p4 = (iter g,(n + k)) . p3 by Lemiter12, B1;
then y1 <= p4 by B1, Lemiter13;
hence p1 <= p4 by B2, ORDERS_2:26; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( p3 = g . p & p <= p3 & p1 = (iter g,n) . p & p4 = (iter g,(n + k)) . p implies p1 <= p4 ) ; :: thesis: verum