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
now :: thesis: for x being object st x in { P where P is Subset of D : ( d0 in P & P <> D ) } holds
x in bool D
let x be object ; :: 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 ex Q being Subset of D st
( x = Q & d0 in Q & Q <> D ) ;
hence x in bool D ; :: thesis: verum
end;
then A1: { P where P is Subset of D : ( d0 in P & P <> D ) } c= bool D by TARSKI:def 3;
reconsider P = {d0} as Subset of D ;
assume A2: STS (D,d0) = 1TopSp D ; :: thesis: D = {d0}
A3: d0 in P by TARSKI:def 1;
assume D <> {d0} ; :: thesis: contradiction
then P in { P where P is Subset of D : ( d0 in P & P <> D ) } by A3;
hence contradiction by A2, A1, 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