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 Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
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 Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
let d be distance_function of A,L; for S being ExtensionSeq2 of A,d
for k, l being Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
let S be ExtensionSeq2 of A,d; for k, l being Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
let k be Element of NAT ; for l being Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
defpred S1[ Element of NAT ] means ( k <= $1 implies (S . k) `1 c= (S . $1) `1 );
A1:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume that A2:
(
k <= i implies
(S . k) `1 c= (S . i) `1 )
and A3:
k <= i + 1
;
(S . k) `1 c= (S . (i + 1)) `1
per cases
( k = i + 1 or k <= i )
by A3, NAT_1:8;
suppose A4:
k <= i
;
(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_extension2_of A9,
d9
and A6:
S . i = [A9,d9]
and A7:
S . (i + 1) = [Aq,dq]
by Def12;
(S . i) `1 = A9
by A6, MCART_1:def 1;
then A8:
(S . i) `1 c= ConsecutiveSet2 (
A9,
(DistEsti d9))
by Th18;
ex
q being
QuadrSeq of
d9 st
(
Aq = NextSet2 d9 &
dq = NextDelta2 q )
by A5, Def11;
then
(S . (i + 1)) `1 = ConsecutiveSet2 (
A9,
(DistEsti d9))
by A7, MCART_1:def 1;
hence
(S . k) `1 c= (S . (i + 1)) `1
by A2, A4, A8, XBOOLE_1:1;
verum end;
end;
A9:
S1[ 0 ]
by NAT_1:3;
thus
for l being Element of NAT holds S1[l]
from NAT_1:sch 1(A9, A1); verum