set T = { S where S is Subset of L : ( S is upper & S is inaccessible_by_directed_joins ) } ;
{ S where S is Subset of L : ( S is upper & S is inaccessible_by_directed_joins ) } c= bool the carrier of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Subset of L : ( S is upper & S is inaccessible_by_directed_joins ) } or x in bool the carrier of L )
assume x in { S where S is Subset of L : ( S is upper & S is inaccessible_by_directed_joins ) } ; :: thesis: x in bool the carrier of L
then ex S being Subset of L st
( x = S & S is upper & S is inaccessible_by_directed_joins ) ;
hence x in bool the carrier of L ; :: thesis: verum

end;

then reconsider T = { S where S is Subset of L : ( S is upper & S is inaccessible_by_directed_joins ) } as Subset-Family of L ;
set SL = TopRelStr(# the carrier of L, the InternalRel of L,T #);
A1: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,T #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,T #) #) ;
then reconsider SL = TopRelStr(# the carrier of L, the InternalRel of L,T #) as TopAugmentation of L by YELLOW_9:def 4;
take SL ; :: thesis: ( SL is strict & SL is Scott )
for S being Subset of SL holds
( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) )

proof

let S be Subset of SL; :: thesis: ( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) )
thus ( S is open implies ( S is inaccessible_by_directed_joins & S is upper ) ) :: thesis: ( S is inaccessible_by_directed_joins & S is upper implies S is open )

proof

assume S is open ; :: thesis: ( S is inaccessible_by_directed_joins & S is upper )
then S in T by PRE_TOPC:def 2;
then ex S1 being Subset of L st
( S1 = S & S1 is upper & S1 is inaccessible_by_directed_joins ) ;
hence ( S is inaccessible_by_directed_joins & S is upper ) by A1, WAYBEL_0:25, YELLOW_9:47; :: thesis: verum

end;

thus ( S is inaccessible_by_directed_joins & S is upper implies S is open ) :: thesis: verum

proof

reconsider S1 = S as Subset of L ;
assume ( S is inaccessible_by_directed_joins & S is upper ) ; :: thesis: S is open
then ( S1 is inaccessible_by_directed_joins & S1 is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;
then S in the topology of SL ;
hence S is open by PRE_TOPC:def 2; :: thesis: verum

end;

end;

hence ( SL is strict & SL is Scott ) by WAYBEL11:def 4; :: thesis: verum