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 ) } ;
((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 A1: 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;
let A be Subset of (STS D,d0); :: thesis: ( A = {d0} implies 1TopSp D = (STS D,d0) modified_with_respect_to A )
assume A2: A = {d0} ; :: thesis: 1TopSp D = (STS D,d0) modified_with_respect_to A
A3: { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS D,d0)

proof

A4: 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

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
A5: W = P and
A6: d0 in P and
P <> D ;
reconsider F = D as Subset of D by Lm1;
set H = P \ {d0};
reconsider H = P \ {d0} as Subset of D ;
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 A7: 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 A8: H in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def 5;
( A c= P & A c= D ) by A2, A6, ZFMISC_1:37;
then ( W = H \/ A & A = F /\ A ) by A2, A5, XBOOLE_1:28, XBOOLE_1:45;
hence W in A -extension_of_the_topology_of (STS D,d0) by A4, A7, A8; :: thesis: verum

end;

hence { 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; :: thesis: verum

end;

(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 A3, XBOOLE_1:8;
then A9: bool D c= A -extension_of_the_topology_of (STS D,d0) by A1, 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 A9, XBOOLE_0:def 10 ;
hence 1TopSp D = (STS D,d0) modified_with_respect_to A by TMAP_1:104; :: thesis: verum