let L be complete Scott TopLattice; :: thesis: 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 )
let X be Subset of L; :: thesis: 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 )
let V be Element of (InclPoset (sigma L)); :: thesis: ( V = X & ex x being Element of L st X = (downarrow x) ` implies ( V is prime & V <> the carrier of L ) )
assume A1: V = X ; :: thesis: ( for x being Element of L holds not X = (downarrow x) ` or ( V is prime & V <> the carrier of L ) )
A2: ( sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) & TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) ) by WAYBEL11:32, WAYBEL11:def 12;
given u being Element of L such that A3: X = (downarrow u) ` ; :: thesis: ( V is prime & V <> the carrier of L )
( Cl {u} = downarrow u & Cl {u} is irreducible ) by WAYBEL11:9, YELLOW_8:17;
hence V is prime by A1, A2, A3, Th17; :: thesis: V <> the carrier of L
assume V = the carrier of L ; :: thesis: contradiction
hence contradiction by A1, A3, Th2; :: thesis: verum