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 Element of 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 Element of 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 Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
let S be ExtensionSeq of A,d; :: thesis: for k, l being Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
let k be Element of NAT ; :: thesis: 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 ;
:: 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 A3, NAT_1:8;
suppose A4:
k <= i
;
:: thesis: (S . k) `1 c= (S . (i + 1)) `1 consider A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq being non
empty set ,
dq being
distance_function of
Aq,
L such that A5:
Aq,
dq is_extension_of A',
d'
and A6:
S . i = [A',d']
and A7:
S . (i + 1) = [Aq,dq]
by Def21;
(S . i) `1 = A'
by A6, MCART_1:def 1;
then A8:
(S . i) `1 c= ConsecutiveSet A',
(DistEsti d')
by Th27;
ex
q being
QuadrSeq of
d' st
(
Aq = NextSet d' &
dq = NextDelta q )
by A5, Def20;
then
(S . (i + 1)) `1 = ConsecutiveSet A',
(DistEsti d')
by A7, MCART_1:def 1;
hence
(S . k) `1 c= (S . (i + 1)) `1
by A2, A4, A8, XBOOLE_1:1;
:: thesis: 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); :: thesis: verum