let L be completely-distributive LATTICE; :: thesis: L is continuous
A1: for J being non empty set
for K being V9() ManySortedSet of J
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;
L is complete by Def3;
hence L is continuous by A1, Lm9; :: thesis: verum