let L be complete Scott TopLattice; :: thesis: ( sup_op L is jointly_Scott-continuous implies L is sober )
assume A1: sup_op L is jointly_Scott-continuous ; :: thesis: L is sober
let S be irreducible Subset of L; :: according to YELLOW_8:def 5 :: thesis: ex b₁ being Element of the carrier of L st
( b₁ is_dense_point_of S & ( for b₂ being Element of the carrier of L holds
( not b₂ is_dense_point_of S or b₁ = b₂ ) ) )
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;
A3: ( not S is empty & S is closed ) by YELLOW_8:def 3;
then ( the carrier of (InclPoset (sigma L)) = sigma L & S ` is open ) by YELLOW_1:1;
then reconsider V = S ` as Element of (InclPoset (sigma L)) by A2, PRE_TOPC:def 2;
S ` <> the carrier of L by Th2;
then consider p being Element of L such that
A4: V = (downarrow p) ` by A1, A2, Th17, Th29;
A5: L is T_0 by WAYBEL11:10;
take p ; :: thesis: ( p is_dense_point_of S & ( for b₁ being Element of the carrier of L holds
( not b₁ is_dense_point_of S or p = b₁ ) ) )
A6: Cl {p} = downarrow p by WAYBEL11:9;
A7: S = downarrow p by A4, TOPS_1:1;
hence p is_dense_point_of S by A6, YELLOW_8:18; :: thesis: for b₁ being Element of the carrier of L holds
( not b₁ is_dense_point_of S or p = b₁ )
let q be Point of L; :: thesis: ( not q is_dense_point_of S or p = q )
assume q is_dense_point_of S ; :: thesis: p = q
then Cl {q} = S by A3, YELLOW_8:16;
hence p = q by A7, A6, A5, YELLOW_8:23; :: thesis: verum