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)

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

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 {X} \/ (bool X0) or a in the topology of (X0 -DiscreteTop X) )
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;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

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