theorem Th38: :: LATTICE5:38

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) `1 c= (S . l) `1