theorem :: WAYBEL14:28

for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )