let A be non empty set ; :: thesis: for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
let L be lower-bounded modular LATTICE; :: thesis: for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
let d be distance_function of A,L; :: thesis: for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
let S be ExtensionSeq2 of A,d; :: thesis: for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
let k be Nat; :: thesis: for l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
defpred S₁[ Nat] means ( k <= $1 implies (S . k) `2 c= (S . $1) `2 );
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) `2 c= (S . i) `2 ) and
A3: k <= i + 1 ; :: thesis: (S . k) `2 c= (S . (i + 1)) `2

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

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

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

end;

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

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_extension2_of A9,d9 and
A6: S . i = [A9,d9] and
A7: S . (i + 1) = [Aq,dq] by Def11;
consider q being QuadrSeq of d9 such that
Aq = NextSet2 d9 and
A8: dq = NextDelta2 q by A5;
A9: (S . i) `2 c= ConsecutiveDelta2 (q,(DistEsti d9)) by Th23, A6;
[Aq,dq] `2 = ConsecutiveDelta2 (q,(DistEsti d9)) by A8;
hence (S . k) `2 c= (S . (i + 1)) `2 by A2, A4, A9, A7; :: thesis: verum

end;

end;

end;

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