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 S1[ Nat] means ( k <= \$1 implies (S . k) `1 c= (S . \$1) `1 );
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[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 ;
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 ;
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: S1[ 0 ] by NAT_1:3;
thus for l being Nat holds S1[l] from NAT_1:sch 2(A9, A1); :: thesis: verum