let L be complete Scott TopLattice; :: thesis: ( ( for x being Element of ex B being Basis of x st
for Y being Subset of st Y in B holds
( Y is open & Y is filtered ) ) iff for V being Element of ex VV being Subset of st
( V = sup VV & ( for W being Element of st W in VV holds
W is co-prime ) ) )
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: ( ( for V being Element of ex VV being Subset of st
( V = sup VV & ( for W being Element of st W in VV holds
W is co-prime ) ) ) implies for x being Element of ex B being Basis of x st
for Y being Subset of st Y in B holds
( Y is open & Y is filtered ) )

assume A3: for x being Element of ex X being Basis of x st
for Y being Subset of st Y in X holds
( Y is open & Y is filtered ) ; :: thesis: for V being Element of ex X being Subset of st
( V = sup X & ( for Yp being Element of st Yp in X holds
Yp is co-prime ) )
let V be Element of ; :: thesis: ex X being Subset of st
( V = sup X & ( for Yp being Element of st Yp in X holds
Yp is co-prime ) )
set X = { Y where Y is Subset of : ( Y c= V & ex x being Element of ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } ;

now

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

end;

then reconsider X = { Y where Y is Subset of : ( Y c= V & ex x being Element of ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } as Subset of by TARSKI:def 3;
take X = X; :: thesis: ( V = sup X & ( for Yp being Element of st Yp in X holds
Yp is co-prime ) )
V in sigma L by A1, A2;
then reconsider Vl = V as Subset of ;
A6: Vl is open by A1, A2, Th24;

now

let x be set ; :: thesis: ( ( x in V implies x in union X ) & ( x in union X implies x in V ) )

hereby :: thesis: ( x in union X implies x in V )

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

end;

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

end;

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

end;

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

proof

let VV be set ; :: according to TARSKI:def 3 :: thesis: ( not VV in { V where V is Element of : ( x in V & V is co-prime ) } or VV in bool the carrier of L )
assume VV in { V where V is Element of : ( x in V & V is co-prime ) } ; :: thesis: VV in bool the carrier of L
then ex V being Element of 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: verum

end;

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

proof

A80: bas is open

proof

let VV be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not VV in bas or VV is open )
assume VV in bas ; :: thesis: VV is open
then ex V being Element of st
( VV = V & x in V & V is co-prime ) ;
hence VV is open by A1, A2, PRE_TOPC:def 5; :: thesis: verum

end;

bas is x -quasi_basis

proof

now

per cases ( bas is empty or not bas is empty ) ;

suppose bas is empty ; :: thesis: x in Intersect bas

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

end;

suppose A18: not bas is empty ; :: thesis: x in Intersect bas

A19: now

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

end;

Intersect bas = meet bas by A18, SETFAM_1:def 10;
hence x in Intersect bas by A18, A19, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

hence x in Intersect bas ; :: according to YELLOW_8:def 2 :: thesis: for b₁ being Element of bool the carrier of L holds
( not b₁ is open or not x in b₁ or ex b₂ being Element of bool the carrier of L st
( b₂ in bas & b₂ c= b₁ ) )
let S be Subset of ; :: thesis: ( not S is open or not x in S or ex b₁ being Element of bool the carrier of L st
( b₁ in bas & b₁ c= S ) )
assume that
A20: S is open and
A21: x in S ; :: thesis: ex b₁ being Element of bool the carrier of L st
( b₁ in bas & b₁ c= S )
reconsider S' = S as Element of by A2, A20, Th24;
consider X being Subset of such that
A22: S' = sup X and
A23: for x being Element of st x in X holds
x is co-prime by A1, A17;
S' = union X by A22, YELLOW_1:22;
then consider V being set such that
A24: x in V and
A25: V in X by A21, TARSKI:def 4;
V in sigma L by A2, A25;
then reconsider V = V as Subset of ;
reconsider Vp = V as Element of by A25;
take V ; :: thesis: ( V in bas & V c= S )
Vp is co-prime by A23, A25;
hence V in bas by A1, A24; :: thesis: V c= S
sup X is_>=_than X by YELLOW_0:32;
then Vp <= sup X by A25, LATTICE3:def 9;
hence V c= S by A22, YELLOW_1:3; :: thesis: verum

end;

hence bas is Basis of x by A80; :: thesis: verum

end;

then reconsider bas = bas as Basis of x ;
take bas ; :: thesis: for Y being Subset of st Y in bas holds
( Y is open & Y is filtered )
let V be Subset of ; :: thesis: ( V in bas implies ( V is open & V is filtered ) )
assume V in bas ; :: thesis: ( V is open & V is filtered )
then ex Vp being Element of st
( V = Vp & x in Vp & Vp is co-prime ) ;
hence ( V is open & V is filtered ) by A1, A2, Th24, Th27; :: thesis: verum