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_{1}[ Nat] means ( k <= $1 implies (S . k) `1 c= (S . $1) `1 );

A1: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by NAT_1:3;

thus for l being Nat holds S_{1}[l]
from NAT_1:sch 2(A9, A1); :: thesis: verum

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

A1: for i being Nat st S

S

proof

A9:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[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

end;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;

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;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

thus for l being Nat holds S