theorem Th25: :: WAYBEL14:25

for L being complete Scott TopLattice
for VV being Subset of (InclPoset (sigma L))
for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds
VV is directed