let X be set ; :: thesis: for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)
let X0 be Subset of X; :: thesis: the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)
A1: the carrier of (X0 -DiscreteTop X) = X by Def8;
thus the topology of (X0 -DiscreteTop X) c= {X} \/ (bool X0) :: according to XBOOLE_0:def 10 :: thesis: {X} \/ (bool X0) c= the topology of (X0 -DiscreteTop X)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of (X0 -DiscreteTop X) or a in {X} \/ (bool X0) )
assume A2: a in the topology of (X0 -DiscreteTop X) ; :: thesis: a in {X} \/ (bool X0)
then reconsider a = a as Subset of (X0 -DiscreteTop X) ;
A3: ( ( a is proper & not X is empty ) or not a is proper ) by A1;
a is open by A2;
then ( a = X or a c= X0 ) by A3, A1, Th43;
then ( a in {X} or a in bool X0 ) by TARSKI:def 1;
hence a in {X} \/ (bool X0) by XBOOLE_0:def 3; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {X} \/ (bool X0) or a in the topology of (X0 -DiscreteTop X) )
reconsider aa = a as set by TARSKI:1;
assume a in {X} \/ (bool X0) ; :: thesis: a in the topology of (X0 -DiscreteTop X)
then A4: ( a in {X} or a in bool X0 ) by XBOOLE_0:def 3;
then ( a = X or aa c= X0 ) by TARSKI:def 1;
then reconsider a = a as Subset of (X0 -DiscreteTop X) by A1, XBOOLE_1:1;
assume A5: not a in the topology of (X0 -DiscreteTop X) ; :: thesis: contradiction
then A6: a <> [#] (X0 -DiscreteTop X) by PRE_TOPC:def 2;
then A7: not X is empty by A1;
A8: a is proper by A6;
A9: not a is open by A5;
a <> X by A6, Def8;
hence contradiction by A7, A4, A9, A8, Th43, TARSKI:def 1; :: thesis: verum