let L be completely-distributive LATTICE; :: thesis: L is continuous
for J being non empty set
for K being V9() ManySortedSet of holds
( L is complete & ( for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) ) by Def3;
hence L is continuous by Lm9; :: thesis: verum