:: deftheorem defines is_extension2_of LATTICE8:def 10 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( Aq,dq is_extension2_of A,d iff ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q ) );