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:3;
then A ` is closed by Th20;
hence A is open by TOPS_1:4; :: 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, Th20;
then (A `) ` c= P ` by SUBSET_1:12;
hence A c= D \ {d0} ; :: thesis: verum

end;