let D be non empty set ; :: thesis: for d0 being Element of D
for A being Subset of (STS (D,d0)) st A = {d0} holds
1TopSp D = (STS (D,d0)) modified_with_respect_to A
let d0 be Element of D; :: thesis: for A being Subset of (STS (D,d0)) st A = {d0} holds
1TopSp D = (STS (D,d0)) modified_with_respect_to A
set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ;
set T = (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ;
let A be Subset of (STS (D,d0)); :: thesis: ( A = {d0} implies 1TopSp D = (STS (D,d0)) modified_with_respect_to A )
assume A1: A = {d0} ; :: thesis: 1TopSp D = (STS (D,d0)) modified_with_respect_to A
A2: A -extension_of_the_topology_of (STS (D,d0)) = { (H \/ (F /\ A)) where H, F is Subset of (STS (D,d0)) : ( H in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } & F in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) } by TMAP_1:def 7;

now :: thesis: for W being object st W in { P where P is Subset of D : ( d0 in P & P <> D ) } holds
W in A -extension_of_the_topology_of (STS (D,d0))

reconsider F = D as Subset of D by Lm1;
let W be object ; :: thesis: ( W in { P where P is Subset of D : ( d0 in P & P <> D ) } implies W in A -extension_of_the_topology_of (STS (D,d0)) )
assume W in { P where P is Subset of D : ( d0 in P & P <> D ) } ; :: thesis: W in A -extension_of_the_topology_of (STS (D,d0))
then consider P being Subset of D such that
A3: W = P and
A4: d0 in P and
P <> D ;
set H = P \ {d0};
reconsider H = P \ {d0} as Subset of D ;
A c= P by A1, A4, ZFMISC_1:31;
then A5: W = H \/ A by A1, A3, XBOOLE_1:45;
for K being Subset of D holds
( not K = F or not d0 in K or not K <> D ) ;
then not F in { P where P is Subset of D : ( d0 in P & P <> D ) } ;
then A6: F in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def 5;
d0 in {d0} by TARSKI:def 1;
then for K being Subset of D holds
( not K = H or not d0 in K or not K <> D ) by XBOOLE_0:def 5;
then not H in { P where P is Subset of D : ( d0 in P & P <> D ) } ;
then A7: H in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def 5;
A = F /\ A by XBOOLE_1:28;
hence W in A -extension_of_the_topology_of (STS (D,d0)) by A2, A6, A7, A5; :: thesis: verum

end;

then A8: { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS (D,d0)) by TARSKI:def 3;
((bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } = (bool D) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_1:39;
then A9: bool D c= ((bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_1:7;
(bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS (D,d0)) by TMAP_1:88;
then ((bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS (D,d0)) by A8, XBOOLE_1:8;
then A10: bool D c= A -extension_of_the_topology_of (STS (D,d0)) by A9, XBOOLE_1:1;
the topology of ((STS (D,d0)) modified_with_respect_to A) = A -extension_of_the_topology_of (STS (D,d0)) by TMAP_1:93
.= the topology of (1TopSp D) by A10, XBOOLE_0:def 10 ;
hence 1TopSp D = (STS (D,d0)) modified_with_respect_to A by TMAP_1:93; :: thesis: verum