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

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 ) )

{ S where S is Subset of L : ( S is upper & S is inaccessible ) } c= bool the carrier of L

proof

then reconsider T = { S where S is Subset of L : ( S is upper & S is inaccessible ) } as Subset-Family of L ;
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;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

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

hence
( SL is strict & SL is Scott )
; :: thesis: verum
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 )

end;thus ( S is open implies ( S is inaccessible & S is upper ) ) :: thesis: ( S is inaccessible & S is upper implies S is open )

proof

thus
( S is inaccessible & S is upper implies S is open )
:: thesis: verum
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 A1, WAYBEL_0:25, YELLOW_9:47; :: thesis: verum

end;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 A1, WAYBEL_0:25, YELLOW_9:47; :: 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 A1, WAYBEL_0:25, YELLOW_9:47;

then S in the topology of SL ;

hence S is open ; :: thesis: verum

end;assume ( S is inaccessible & S is upper ) ; :: thesis: S is open

then ( S1 is inaccessible & S1 is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;

then S in the topology of SL ;

hence S is open ; :: thesis: verum