let L be complete Scott TopLattice; :: thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
let X be Subset of L; :: thesis: for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
let V be Element of (InclPoset (sigma L)); :: thesis: ( V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L implies ex x being Element of L st X = (downarrow x) ` )
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: ex x being Element of L st X = (downarrow x) `
A5: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
set A = X ` ;
A6: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def 12;
A7: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A8: X is open by A1, A6, A5, PRE_TOPC:def 2;
then X ` is closed ;
then A9: ( X ` is directly_closed & X ` is lower ) by WAYBEL11:7;
A10: X ` is directed

proof

set LxL = [:L,L:];
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: contradiction
( 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;
consider Tsup being Function of [:L,L:],L such that
A14: Tsup = sup_op L and
A15: Tsup is continuous by A2, A5;
A16: Tsup . (a,b) = a "\/" b by A14, WAYBEL_2:def 5;
[#] L <> {} ;
then Tsup " X is open by A8, A15, TOPS_2:43;
then consider AA being Subset-Family of [:L,L:] such that
A17: Tsup " X = union AA and
A18: 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 BORSUK_1:5;
A19: the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by BORSUK_1:def 2;
then [a,b] in the carrier of [:L,L:] by ZFMISC_1:def 2;
then [a,b] in Tsup " X by A13, A16, FUNCT_2:38;
then consider AAe being set such that
A20: [a,b] in AAe and
A21: AAe in AA by A17, TARSKI:def 4;
consider Va, Vb being Subset of L such that
A22: AAe = [:Va,Vb:] and
A23: Va is open and
A24: Vb is open by A18, A21;
A25: ( a in Va & b in Vb ) by A20, A22, ZFMISC_1:87;
reconsider Va9 = Va, Vb9 = Vb as Subset of L ;

now :: thesis: for x being object holds
( ( x in Tsup .: AAe implies x in Va /\ Vb ) & ( x in Va /\ Vb implies x in Tsup .: AAe ) )

let x be object ; :: thesis: ( ( x in Tsup .: AAe implies x in Va /\ Vb ) & ( x in Va /\ Vb implies x in Tsup .: AAe ) )

hereby :: thesis: ( x in Va /\ Vb implies x in Tsup .: AAe )

assume x in Tsup .: AAe ; :: thesis: x in Va /\ Vb
then consider cd being object such that
A26: cd in the carrier of [:L,L:] and
A27: cd in AAe and
A28: Tsup . cd = x by FUNCT_2:64;
consider c, d being Element of L such that
A29: cd = [c,d] by A19, A26, DOMAIN_1:1;
reconsider c = c, d = d as Element of L ;
A30: x = Tsup . (c,d) by A28, A29
.= c "\/" d by A14, WAYBEL_2:def 5 ;
A31: ( d <= c "\/" d & Vb9 is upper ) by A24, WAYBEL11:def 4, YELLOW_0:22;
d in Vb by A22, A27, A29, ZFMISC_1:87;
then A32: x in Vb by A30, A31;
A33: ( c <= c "\/" d & Va9 is upper ) by A23, WAYBEL11:def 4, YELLOW_0:22;
c in Va by A22, A27, A29, ZFMISC_1:87;
then x in Va by A30, A33;
hence x in Va /\ Vb by A32, XBOOLE_0:def 4; :: thesis: verum

end;

assume A34: x in Va /\ Vb ; :: thesis: x in Tsup .: AAe
then reconsider c = x as Element of L ;
( x in Va & x in Vb ) by A34, XBOOLE_0:def 4;
then A35: [c,c] in AAe by A22, ZFMISC_1:87;
c <= c ;
then c = c "\/" c by YELLOW_0:24;
then A36: c = Tsup . (c,c) by A14, WAYBEL_2:def 5;
[c,c] in the carrier of [:L,L:] by A19, ZFMISC_1:87;
hence x in Tsup .: AAe by A35, A36, FUNCT_2:35; :: thesis: verum

end;

then A37: Tsup .: AAe = Va /\ Vb by TARSKI:2;
A38: Tsup .: (Tsup " X) c= X by FUNCT_1:75;
Tsup .: AAe c= Tsup .: (Tsup " X) by A17, A21, RELAT_1:123, ZFMISC_1:74;
then A39: Tsup .: AAe c= X by A38;
( Va in sigma L & Vb in sigma L ) by A6, A5, A23, A24, PRE_TOPC:def 2;
then ( Va c= X or Vb c= X ) by A1, A3, A6, A7, A37, A39, Th19;
hence contradiction by A11, A25, XBOOLE_0:def 5; :: thesis: verum

end;

take u = sup (X `); :: thesis: X = (downarrow u) `

now :: thesis: not X ` = {}

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

end;

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