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} ) )
reconsider P = {d0} as Subset of (STS (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 ` ;
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 Th22; :: thesis: A is dense
([#] (STS (D,d0))) \ (([#] (STS (D,d0))) \ P) = A ` by A2;
then P = A ` by PRE_TOPC:3;
then A ` is boundary by A1, Th21;
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 A4: A is open ; :: thesis: ( not A is dense or A = D \ {d0} )
assume A is dense ; :: thesis: A = D \ {d0}
then A ` is boundary by TOPS_3:18;
then A ` = {d0} by A1, A3, A4, Th21;
then A = P ` ;
hence A = D \ {d0} ; :: thesis: verum
end;