let D be non empty set ; :: thesis: for d0 being Element of D holds
( STS D,d0 = 1TopSp D iff D = {d0} )
let d0 be Element of D; :: thesis: ( STS D,d0 = 1TopSp D iff D = {d0} )
set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ;
thus ( STS D,d0 = 1TopSp D implies D = {d0} ) :: thesis: ( D = {d0} implies STS D,d0 = 1TopSp D )

proof

assume A1: STS D,d0 = 1TopSp D ; :: thesis: D = {d0}
A2: { P where P is Subset of D : ( d0 in P & P <> D ) } c= bool D

proof

now

let x be set ; :: thesis: ( x in { P where P is Subset of D : ( d0 in P & P <> D ) } implies x in bool D )
assume x in { P where P is Subset of D : ( d0 in P & P <> D ) } ; :: thesis: x in bool D
then consider Q being Subset of D such that
A3: x = Q and
( d0 in Q & Q <> D ) ;
thus x in bool D by A3; :: thesis: verum

end;

hence { P where P is Subset of D : ( d0 in P & P <> D ) } c= bool D by TARSKI:def 3; :: thesis: verum

end;

assume A4: D <> {d0} ; :: thesis: contradiction
reconsider P = {d0} as Subset of D ;
d0 in P by TARSKI:def 1;
then P in { P where P is Subset of D : ( d0 in P & P <> D ) } by A4;
hence contradiction by A1, A2, XBOOLE_1:38; :: thesis: verum

end;

assume D = {d0} ; :: thesis: STS D,d0 = 1TopSp D
then { P where P is Subset of D : ( d0 in P & P <> D ) } = {} by Lm2;
hence STS D,d0 = 1TopSp D ; :: thesis: verum