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)) by WAYBEL11:def 12;
A3: TopStruct(# the carrier of L,the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
given u being Element of L such that A4: X = (downarrow u) ` ; :: thesis: ( V is prime & V <> the carrier of L )
A5: Cl {u} = downarrow u by WAYBEL11:9;
Cl {u} is irreducible by YELLOW_8:26;
hence V is prime by A1, A2, A3, A4, A5, Th17; :: thesis: V <> the carrier of L
assume V = the carrier of L ; :: thesis: contradiction
hence contradiction by A1, A4, Th2; :: thesis: verum