theorem Th39: :: LATTICE5:39

for A being non empty set
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) `2 c= (S . l) `2