let D be non empty set ; :: thesis: for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS D,d0) holds
( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )
let d0 be Element of D; :: thesis: ( not D \ {d0} is empty implies for A being Subset of (STS D,d0) holds
( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) ) )
assume A1: not D \ {d0} is empty ; :: thesis: for A being Subset of (STS D,d0) holds
( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )
let A be Subset of (STS D,d0); :: thesis: ( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )
set Z = A ` ;
reconsider P = {d0} as Subset of (STS D,d0) ;
thus ( A = D \ {d0} implies ( A is open & A is dense ) ) :: thesis: ( A <> D & A is open & A is dense implies A = D \ {d0} )

proof

assume A2: A = D \ {d0} ; :: thesis: ( A is open & A is dense )
hence A is open by Th26; :: thesis: A is dense
([#] (STS D,d0)) \ (([#] (STS D,d0)) \ P) = A ` by A2;
then P = A ` by PRE_TOPC:22;
then ( A ` is closed & A ` is boundary ) by A1, Th25;
hence A is dense by TOPS_3:18; :: thesis: verum

end;

thus ( A <> D & A is open & A is dense implies A = D \ {d0} ) :: thesis: verum

proof

assume A <> D ; :: thesis: ( not A is open or not A is dense or A = D \ {d0} )
then A3: A ` <> {} (STS D,d0) by TOPS_3:2;
assume A is open ; :: thesis: ( not A is dense or A = D \ {d0} )
then A4: A ` is closed ;
assume A is dense ; :: thesis: A = D \ {d0}
then A ` is boundary by TOPS_3:18;
then A ` = {d0} by A1, A3, A4, Th25;
then A = P ` ;
hence A = D \ {d0} ; :: thesis: verum

end;