let D be non empty set ; :: thesis: for d0 being Element of D
for A being Subset of (STS (D,d0)) holds
( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )
let d0 be Element of D; :: thesis: for A being Subset of (STS (D,d0)) holds
( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )
let A be Subset of (STS (D,d0)); :: thesis: ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )
set Z = A ` ;
set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ;
thus ( {d0} c= A implies A is closed ) :: thesis: ( not A is empty & A is closed implies {d0} c= A )
proof
A1: d0 in {d0} by TARSKI:def 1;
assume {d0} c= A ; :: thesis: A is closed
then for Q being Subset of D holds
( not Q = A ` or not d0 in Q or not Q <> D ) by A1, XBOOLE_0:def 5;
then not A ` in { P where P is Subset of D : ( d0 in P & P <> D ) } ;
then A ` in the topology of (STS (D,d0)) by XBOOLE_0:def 5;
then A ` is open ;
hence A is closed ; :: thesis: verum
end;
assume not A is empty ; :: thesis: ( not A is closed or {d0} c= A )
then A2: A ` <> D by TOPS_3:1;
assume A is closed ; :: thesis: {d0} c= A
then A ` in the topology of (STS (D,d0)) by PRE_TOPC:def 2;
then not A ` in { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def 5;
then not d0 in A ` by A2;
then d0 in A by SUBSET_1:29;
hence {d0} c= A by ZFMISC_1:31; :: thesis: verum