let L be complete LATTICE; :: thesis: ( ( 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 ) implies L is continuous )

assume 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 ; :: thesis: L is continuous

then for J being non empty set st J in the_universe_of the carrier of L holds

for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds

for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup ;

hence L is continuous by Th18; :: thesis: verum

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 ) implies L is continuous )

assume 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 ; :: thesis: L is continuous

then for J being non empty set st J in the_universe_of the carrier of L holds

for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds

for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup ;

hence L is continuous by Th18; :: thesis: verum