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

reconsider F = D as Subset of D by Lm1;
let W be set ; :: 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:37;
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:99;
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:104
.= 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:104; :: thesis: verum