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

proof

assume A c= D \ {d0} ; :: thesis: A is open
then ([#] (STS D,d0)) \ (D \ {d0}) c= ([#] (STS D,d0)) \ A by XBOOLE_1:34;
then P c= A ` by PRE_TOPC:22;
then A ` is closed by Th24;
hence A is open by TOPS_1:30; :: thesis: verum

end;

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

proof

assume A <> D ; :: thesis: ( not A is open or A c= D \ {d0} )
then A1: A ` <> {} (STS D,d0) by TOPS_3:2;
assume A is open ; :: thesis: A c= D \ {d0}
then {d0} c= A ` by A1, Th24;
then (A ` ) ` c= P ` by SUBSET_1:31;
hence A c= D \ {d0} ; :: thesis: verum

end;