let L be complete Scott TopLattice; :: thesis:
set IPs = InclPoset the topology of L;
A1: sigma L = the topology of L by Th23;
then A2: the carrier of (InclPoset the topology of L) = sigma L by YELLOW_1:1;

hereby :: thesis:

assume A3: for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered ) ; :: thesis:
let V be Element of (InclPoset (sigma L)); :: thesis:
V in sigma L by A1, A2;
then reconsider Vl = V as Subset of L ;
A4: Vl is open by A1, A2, Th24;
set X = { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } ;

now

let YY be set ; :: thesis:
assume YY in { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } ; :: thesis:
then consider Y being Subset of L such that
A5: Y = YY and
Y c= V and
A6: ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ;
consider x being Element of L, bas being Basis of x such that
A7: ( x in V & Y in bas ) by A6;
Y is open by A7, YELLOW_8:21;
then Y in sigma L by Th24;
hence YY in the carrier of (InclPoset (sigma L)) by A5, YELLOW_1:1; :: thesis:

end;

then reconsider X = { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } as Subset of (InclPoset (sigma L)) by TARSKI:def 3;
take X = X; :: thesis:

now

let x be set ; :: thesis:

hereby :: thesis:

assume A8: x in V ; :: thesis:
Vl = V ;
then reconsider d = x as Element of L by A8;
consider bas being Basis of d such that
A9: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A3;
consider Y being Subset of L such that
A10: ( Y in bas & Y c= V ) by A4, A8, YELLOW_8:22;
( x in Y & Y in X ) by A8, A9, A10, YELLOW_8:21;
hence x in union X by TARSKI:def 4; :: thesis:

end;

assume x in union X ; :: thesis:
then consider YY being set such that
A11: ( x in YY & YY in X ) by TARSKI:def 4;
consider Y being Subset of L such that
A12: Y = YY and
A13: Y c= V and
ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) by A11;
thus x in V by A11, A12, A13; :: thesis:

end;

then V = union X by TARSKI:2;
hence V = sup X by A1, YELLOW_1:22; :: thesis:
let Yp be Element of (InclPoset (sigma L)); :: thesis:
assume Yp in X ; :: thesis:
then consider Y being Subset of L such that
A14: Y = Yp and
Y c= V and
A15: ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ;
consider x being Element of L, bas being Basis of x such that
x in V and
A16: Y in bas and
A17: for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) by A15;
A18: ( Y is open & Y is filtered ) by A16, A17;
then Y is upper by WAYBEL11:def 4;
hence Yp is co-prime by A14, A18, Th27; :: thesis:

end;

assume A19: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) ) ; :: thesis:
let x be Element of L; :: thesis:
set bas = { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } ;
{ V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } c= bool the carrier of L

proof

let VV be set ; :: according to TARSKI:def 3 :: thesis:
assume VV in { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } ; :: thesis:
then ex V being Element of (InclPoset (sigma L)) st
( VV = V & x in V & V is co-prime ) ;
then VV in sigma L by A1, A2;
hence VV in bool the carrier of L ; :: thesis:

end;

then reconsider bas = { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } as Subset-Family of L ;
reconsider bas = bas as Subset-Family of L ;
bas is Basis of x

proof

thus bas c= the topology of L :: according to YELLOW_8:def 2 :: thesis:

proof

let VV be set ; :: according to TARSKI:def 3 :: thesis:
assume VV in bas ; :: thesis:
then ex V being Element of (InclPoset (sigma L)) st
( VV = V & x in V & V is co-prime ) ;
hence VV in the topology of L by A1, A2; :: thesis:

end;

now

per cases ;

suppose bas is empty ; :: thesis:

then Intersect bas = the carrier of L by SETFAM_1:def 10;
hence x in Intersect bas ; :: thesis:

end;

suppose A20: not bas is empty ; :: thesis:

then A21: Intersect bas = meet bas by SETFAM_1:def 10;

now

let Y be set ; :: thesis:
assume Y in bas ; :: thesis:
then ex V being Element of (InclPoset (sigma L)) st
( Y = V & x in V & V is co-prime ) ;
hence x in Y ; :: thesis:

end;

hence x in Intersect bas by A20, A21, SETFAM_1:def 1; :: thesis:

end;

hence x in Intersect bas ; :: thesis:
let S be Subset of L; :: thesis:
assume A22: ( S is open & x in S ) ; :: thesis:
then reconsider S' = S as Element of (InclPoset the topology of L) by A2, Th24;
consider X being Subset of (InclPoset the topology of L) such that
A23: S' = sup X and
A24: for x being Element of (InclPoset the topology of L) st x in X holds
x is co-prime by A1, A19;
S' = union X by A23, YELLOW_1:22;
then consider V being set such that
A25: ( x in V & V in X ) by A22, TARSKI:def 4;
V in sigma L by A2, A25;
then reconsider V = V as Subset of L ;
reconsider Vp = V as Element of (InclPoset the topology of L) by A25;
take V ; :: thesis:
Vp is co-prime by A24, A25;
hence V in bas by A1, A25; :: thesis:
sup X is_>=_than X by YELLOW_0:32;
then Vp <= sup X by A25, LATTICE3:def 9;
hence V c= S by A23, YELLOW_1:3; :: thesis:

end;

then reconsider bas = bas as Basis of x ;
take bas ; :: thesis:
let V be Subset of L; :: thesis:
assume V in bas ; :: thesis:
then consider Vp being Element of (InclPoset (sigma L)) such that
A26: V = Vp and
x in Vp and
A27: Vp is co-prime ;
thus ( V is open & V is filtered ) by A1, A2, A26, A27, Th24, Th27; :: thesis: