:: deftheorem Def11 defines ExtensionSeq2 LATTICE8:def 11 :
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for b₄ being Function holds
( b₄ is ExtensionSeq2 of A,d iff ( dom b₄ = NAT & b₄ . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & b₄ . n = [A9,d9] & b₄ . (n + 1) = [Aq,dq] ) ) ) );