let T be TopSpace; :: thesis: for A being Subset of T st T is T_1 & A is discrete holds
A is open Subset of (T | (Cl A))
let A be Subset of T; :: thesis: ( T is T_1 & A is discrete implies A is open Subset of (T | (Cl A)) )
assume that
A1: T is T_1 and
A2: A is discrete ; :: thesis: A is open Subset of (T | (Cl A))
set TA = T | (Cl A);
A3: [#] (T | (Cl A)) = Cl A by PRE_TOPC:def 5;
A4: A c= Cl A by PRE_TOPC:18;

per cases ( T | (Cl A) is empty or not T | (Cl A) is empty ) ;

suppose T | (Cl A) is empty ; :: thesis: A is open Subset of (T | (Cl A))

hence A is open Subset of (T | (Cl A)) by A3, PRE_TOPC:18; :: thesis: verum

end;

suppose not T | (Cl A) is empty ; :: thesis: A is open Subset of (T | (Cl A))

then reconsider TA = T | (Cl A) as non empty TopSpace ;
deffunc H₁( Element of TA) -> Element of bool the carrier of TA = {$1};
defpred S₁[ set ] means $1 in A;
consider S being Subset-Family of TA such that
A5: S = { H₁(x) where x is Element of TA : S₁[x] } from LMOD_7:sch 5();
A6: S is open

proof

let B be Subset of TA; :: according to TOPS_2:def 1 :: thesis: ( not B in S or B is open )
assume B in S ; :: thesis: B is open
then consider y being Element of TA such that
A7: B = H₁(y) and
A8: S₁[y] by A5;
reconsider x = y as Point of T by A8;
consider G being Subset of T such that
A9: G is open and
A10: A /\ G = {x} by A2, A8, TEX_2:26;
reconsider X = {x} as Subset of T by A10;
not T is empty by A7;
then A11: Cl X = X by A1, PRE_TOPC:22;
x in {x} by TARSKI:def 1;
then ( x in A & x in G ) by A10, XBOOLE_0:def 4;
then A12: G /\ (Cl A) <> {} by A4, XBOOLE_0:def 4;
G /\ (Cl A) c= Cl X by A9, A10, TOPS_1:13;
then G /\ (Cl A) = X by A11, A12, ZFMISC_1:33;
hence B is open by A3, A7, A9, TSP_1:def 1; :: thesis: verum

end;

union S = A

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= union S

let x be object ; :: thesis: ( x in union S implies x in A )
assume x in union S ; :: thesis: x in A
then consider y being set such that
A13: x in y and
A14: y in S by TARSKI:def 4;
ex z being Element of TA st
( H₁(z) = y & S₁[z] ) by A5, A14;
hence x in A by A13, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union S )
assume x in A ; :: thesis: x in union S
then A15: {x} in S by A3, A4, A5;
x in {x} by TARSKI:def 1;
hence x in union S by A15, TARSKI:def 4; :: thesis: verum

end;

hence A is open Subset of (T | (Cl A)) by A6, TOPS_2:19; :: thesis: verum

end;

end;