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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } ; :: thesis:
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:

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:
for S being Subset of SL holds
( S is open iff ( S is inaccessible & S is upper ) )

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

end;

end;