theorem Th30: :: LATTICE8:30

for A being 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 Nat st k <= l holds
(S . k) `1 c= (S . l) `1