let L be complete Scott TopLattice; ( sup_op L is jointly_Scott-continuous implies L is sober )
assume A1:
sup_op L is jointly_Scott-continuous
; L is sober
let S be irreducible Subset of L; YELLOW_8:def 5 ex b1 being Element of the carrier of L st
( b1 is_dense_point_of S & ( for b2 being Element of the carrier of L holds
( not b2 is_dense_point_of S or b1 = b2 ) ) )
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
; ( p is_dense_point_of S & ( for b1 being Element of the carrier of L holds
( not b1 is_dense_point_of S or p = b1 ) ) )
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; for b1 being Element of the carrier of L holds
( not b1 is_dense_point_of S or p = b1 )
let q be Point of L; ( not q is_dense_point_of S or p = q )
assume
q is_dense_point_of S
; p = q
then
Cl {q} = S
by A3, YELLOW_8:16;
hence
p = q
by A7, A6, A5, YELLOW_8:23; verum