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
A2: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def 12;
A3: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
A4: TopStruct(# the carrier of L,the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
let S be irreducible Subset of L; :: according to YELLOW_8:def 6 :: 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₂ ) ) )
A5: ( not S is empty & S is closed ) by YELLOW_8:def 4;
then A6: S ` is open by TOPS_1:29;
A7: S ` <> the carrier of L by Th2;
reconsider V = S ` as Element of (InclPoset (sigma L)) by A2, A3, A4, A6, PRE_TOPC:def 5;
consider p being Element of L such that
A8: V = (downarrow p) ` by A1, A7, Th29, A2, A4, Th17;
A9: S = downarrow p by A8, TOPS_1:21;
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₁ ) ) )
A10: Cl {p} = downarrow p by WAYBEL11:9;
hence p is_dense_point_of S by A9, YELLOW_8:27; :: 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 A11: Cl {q} = S by A5, YELLOW_8:25;
L is T_0 by WAYBEL11:10;
hence p = q by A9, A10, A11, YELLOW_8:32; :: thesis: verum