let L be complete Scott TopLattice; :: thesis:
let X be Subset of L; :: thesis:
let V be Element of (InclPoset (sigma L)); :: thesis:
assume that
A1: V = X and
A2: sup_op L is jointly_Scott-continuous and
A3: V is prime and
A4: V <> the carrier of L ; :: thesis:
A5: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def 12;
A6: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
A7: TopStruct(# the carrier of L,the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
then A8: X is open by A1, A5, A6, PRE_TOPC:def 5;
set A = X ` ;
X ` is closed by A8, TOPS_1:30;
then A9: ( X ` is closed_under_directed_sups & X ` is lower ) by WAYBEL11:7;
take u = sup (X ` ); :: thesis:
A10: X ` is directed

proof

given a, b being Element of L such that A11: ( a in X ` & b in X ` ) and
A12: for z being Element of L holds
( not z in X ` or not a <= z or not b <= z ) ; :: according to WAYBEL_0:def 1 :: thesis:
( a <= a "\/" b & b <= a "\/" b ) by YELLOW_0:22;
then not a "\/" b in X ` by A12;
then A13: a "\/" b in X by XBOOLE_0:def 5;
set LxL = [:L,L:];
consider Tsup being Function of [:L,L:],L such that
A14: ( Tsup = sup_op L & Tsup is continuous ) by A2, A7, Def1;
[#] L <> {} ;
then A15: Tsup " X is open by A8, A14, TOPS_2:55;
A16: the carrier of [:L,L:] = [:the carrier of L,the carrier of L:] by BORSUK_1:def 5;
then A17: [a,b] in the carrier of [:L,L:] by ZFMISC_1:def 2;
Tsup . a,b = a "\/" b by A14, WAYBEL_2:def 5;
then A18: [a,b] in Tsup " X by A13, A17, FUNCT_2:46;
consider AA being Subset-Family of [:L,L:] such that
A19: Tsup " X = union AA and
A20: for e being set st e in AA holds
ex X1, Y1 being Subset of L st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A15, BORSUK_1:45;
consider AAe being set such that
A21: ( [a,b] in AAe & AAe in AA ) by A18, A19, TARSKI:def 4;
consider Va, Vb being Subset of L such that
A22: ( AAe = [:Va,Vb:] & Va is open & Vb is open ) by A20, A21;
reconsider Va' = Va, Vb' = Vb as Subset of L ;

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in Tsup .: AAe ; :: thesis:
then consider cd being set such that
A23: cd in the carrier of [:L,L:] and
A24: ( cd in AAe & Tsup . cd = x ) by FUNCT_2:115;
consider c, d being Element of L such that
A25: cd = [c,d] by A16, A23, DOMAIN_1:9;
reconsider c = c, d = d as Element of L ;
A26: x = Tsup . c,d by A24, A25
.= c "\/" d by A14, WAYBEL_2:def 5 ;
A27: ( c <= c "\/" d & d <= c "\/" d ) by YELLOW_0:22;
A28: ( Va' is upper & Vb' is upper ) by A22, WAYBEL11:def 4;
( c in Va & d in Vb ) by A22, A24, A25, ZFMISC_1:106;
then ( x in Va & x in Vb ) by A26, A27, A28, WAYBEL_0:def 20;
hence x in Va /\ Vb by XBOOLE_0:def 4; :: thesis:

end;

assume A29: x in Va /\ Vb ; :: thesis:
then A30: ( x in Va & x in Vb ) by XBOOLE_0:def 4;
reconsider c = x as Element of L by A29;
A31: [c,c] in AAe by A22, A30, ZFMISC_1:106;
A32: [c,c] in the carrier of [:L,L:] by A16, ZFMISC_1:106;
c <= c ;
then c = c "\/" c by YELLOW_0:24;
then c = Tsup . c,c by A14, WAYBEL_2:def 5;
hence x in Tsup .: AAe by A31, A32, FUNCT_2:43; :: thesis:

end;

then A33: Tsup .: AAe = Va /\ Vb by TARSKI:2;
AAe c= union AA by A21, ZFMISC_1:92;
then ( Tsup .: AAe c= Tsup .: (Tsup " X) & Tsup .: (Tsup " X) c= X ) by A19, FUNCT_1:145, RELAT_1:156;
then A34: Tsup .: AAe c= X by XBOOLE_1:1;
( Va in sigma L & Vb in sigma L ) by A5, A7, A22, PRE_TOPC:def 5;
then A35: ( Va c= X or Vb c= X ) by A1, A3, A5, A6, A33, A34, Th19;
( a in Va & b in Vb ) by A21, A22, ZFMISC_1:106;
hence contradiction by A11, A35, XBOOLE_0:def 5; :: thesis:

end;

now

assume X ` = {} ; :: thesis:
then (X ` ) ` = the carrier of L ;
hence contradiction by A1, A4; :: thesis:

end;

then u in X ` by A9, A10, WAYBEL11:def 2;
then X ` = downarrow u by A9, Th5;
hence X = (downarrow u) ` ; :: thesis: