let A be non empty set ; 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; 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; 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; for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
let k be Nat; for l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
defpred S1[ Nat] means ( k <= $1 implies (S . k) `2 c= (S . $1) `2 );
A1:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A2:
(
k <= i implies
(S . k) `2 c= (S . i) `2 )
and A3:
k <= i + 1
;
(S . k) `2 c= (S . (i + 1)) `2
per cases
( k = i + 1 or k <= i )
by A3, NAT_1:8;
suppose A4:
k <= i
;
(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;
verum end;
end;
A10:
S1[ 0 ]
by NAT_1:3;
thus
for l being Nat holds S1[l]
from NAT_1:sch 2(A10, A1); verum