let D be non empty set ; 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; 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)); ( A = {d0} implies 1TopSp D = (STS (D,d0)) modified_with_respect_to A )
assume A1:
A = {d0}
; 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 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 ;
( 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 ) }
;
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;
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; verum