let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L
for S being ExtensionSeq of A,d
for k, l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L
for S being ExtensionSeq of A,d
for k, l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1
let d be distance_function of A,L; :: thesis: for S being ExtensionSeq of A,d
for k, l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1
let S be ExtensionSeq of A,d; :: thesis: for k, l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1
let k be Nat; :: thesis: for l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1
defpred S₁[ Nat] means ( k <= $1 implies (S . k) `1 c= (S . $1) `1 );
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A2: ( k <= i implies (S . k) `1 c= (S . i) `1 ) and
A3: k <= i + 1 ; :: thesis: (S . k) `1 c= (S . (i + 1)) `1

per cases ( k = i + 1 or k <= i ) by A3, NAT_1:8;

suppose k = i + 1 ; :: thesis: (S . k) `1 c= (S . (i + 1)) `1

hence (S . k) `1 c= (S . (i + 1)) `1 ; :: thesis: verum

end;

suppose A4: k <= i ; :: thesis: (S . k) `1 c= (S . (i + 1)) `1

consider A9 being non empty set , d9 being distance_function of A9,L, Aq being non empty set , dq being distance_function of Aq,L such that
A5: Aq,dq is_extension_of A9,d9 and
A6: S . i = [A9,d9] and
A7: S . (i + 1) = [Aq,dq] by Def20;
A8: (S . i) `1 c= ConsecutiveSet (A9,(DistEsti d9)) by Th24, A6;
ex q being QuadrSeq of d9 st
( Aq = NextSet d9 & dq = NextDelta q ) by A5;
then (S . (i + 1)) `1 = ConsecutiveSet (A9,(DistEsti d9)) by A7;
hence (S . k) `1 c= (S . (i + 1)) `1 by A2, A4, A8; :: thesis: verum

end;

end;

end;

A9: S₁[ 0 ] by NAT_1:3;
thus for l being Nat holds S₁[l] from NAT_1:sch 2(A9, A1); :: thesis: verum