set T = { S where S is Subset of L : ( S is upper & S is inaccessible ) } ;
{ S where S is Subset of L : ( S is upper & S is inaccessible ) } c= bool the carrier of L
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } or x in bool the carrier of L )
assume x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } ; :: thesis: x in bool the carrier of L
then ex S being Subset of L st
( x = S & S is upper & S is inaccessible ) ;
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 ) } 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 & S is upper ) )
proof
let S be Subset of SL; :: thesis: ( S is open iff ( S is inaccessible & S is upper ) )
thus ( S is open implies ( S is inaccessible & S is upper ) ) :: thesis: ( S is inaccessible & S is upper implies S is open )
proof
assume S is open ; :: thesis: ( S is inaccessible & S is upper )
then S in T ;
then ex S1 being Subset of L st
( S1 = S & S1 is upper & S1 is inaccessible ) ;
hence ( S is inaccessible & S is upper ) by ; :: thesis: verum
end;
thus ( S is inaccessible & S is upper implies S is open ) :: thesis: verum
proof
reconsider S1 = S as Subset of L ;
assume ( S is inaccessible & S is upper ) ; :: thesis: S is open
then ( S1 is inaccessible & S1 is upper ) by ;
then S in the topology of SL ;
hence S is open ; :: thesis: verum
end;
end;
hence ( SL is strict & SL is Scott ) ; :: thesis: verum