:: TOPGEN_1 semantic presentation

begin

theorem Th1: :: TOPGEN_1:1
for T being 1-sorted
for A, B being Subset of T holds
( A meets B ` iff A \ B <> {} )
proof
let T be 1-sorted ; ::_thesis: for A, B being Subset of T holds
( A meets B ` iff A \ B <> {} )
let A, B be Subset of T; ::_thesis: ( A meets B ` iff A \ B <> {} )
hereby  ::_thesis: ( A \ B <> {} implies A meets B ` )
assume  A meets B ` ; ::_thesis: A \ B <> {}
then  A /\ (B `) <> {} by XBOOLE_0:def_7;
hence  A \ B <> {} by SUBSET_1:13; ::_thesis: verum
end;
assume  A \ B <> {} ; ::_thesis: A meets B `
then  A /\ (B `) <> {} by SUBSET_1:13;
hence  A meets B ` by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: TOPGEN_1:2
for T being 1-sorted holds
( T is countable iff card ([#] T) c= omega )
proof
let T be 1-sorted ; ::_thesis: ( T is countable iff card ([#] T) c= omega )
hereby  ::_thesis: ( card ([#] T) c= omega implies T is countable )
assume  T is countable ; ::_thesis: card ([#] T) c= omega
then  [#] T is countable by ORDERS_4:def_2;
hence  card ([#] T) c= omega by CARD_3:def_14; ::_thesis: verum
end;
assume  card ([#] T) c= omega ; ::_thesis: T is countable
then  [#] T is countable by CARD_3:def_14;
hence  T is countable by ORDERS_4:def_2; ::_thesis: verum
end;

registration
let T be finite 1-sorted ;
cluster [#] T ->  finite ;
coherence
 [#] T is finite ;
end;

registration
cluster finite  ->  countable for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is finite holds
b1 is countable
proof
let T be 1-sorted ; ::_thesis: ( T is finite implies T is countable )
assume  T is finite ; ::_thesis: T is countable
then  the carrier of T is countable by CARD_4:1;
hence  T is countable by ORDERS_4:def_2; ::_thesis: verum
end;
end;

registration
cluster non empty countable for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is countable & not b1 is empty )
proof
set T = the non empty finite 1-sorted ;
take  the non empty finite 1-sorted ; ::_thesis: ( the non empty finite 1-sorted is countable & not the non empty finite 1-sorted is empty )
thus  ( the non empty finite 1-sorted is countable & not the non empty finite 1-sorted is empty ) ; ::_thesis: verum
end;
cluster non empty TopSpace-like countable for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is countable & not b1 is empty )
proof
set T = the non empty finite TopSpace;
take  the non empty finite TopSpace ; ::_thesis: ( the non empty finite TopSpace is countable & not the non empty finite TopSpace is empty )
thus  ( the non empty finite TopSpace is countable & not the non empty finite TopSpace is empty ) ; ::_thesis: verum
end;
end;

registration
let T be countable 1-sorted ;
cluster [#] T ->  countable ;
coherence
 [#] T is countable by ORDERS_4:def_2;
end;

registration
cluster non empty TopSpace-like T_1 for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is T_1 & not b1 is empty )
proof
set T = the non empty discrete TopSpace;
take  the non empty discrete TopSpace ; ::_thesis: ( the non empty discrete TopSpace is T_1 & not the non empty discrete TopSpace is empty )
thus  ( the non empty discrete TopSpace is T_1 & not the non empty discrete TopSpace is empty ) ; ::_thesis: verum
end;
end;

begin

theorem Th3: :: TOPGEN_1:3
for T being TopSpace
for A being Subset of T holds Int A = (Cl (A `)) `
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Int A = (Cl (A `)) `
let A be Subset of T; ::_thesis: Int A = (Cl (A `)) `
Int A = (Cl (((A `) `) `)) ` by TDLAT_3:3
.= (Cl (A `)) ` ;
hence  Int A = (Cl (A `)) ` ; ::_thesis: verum
end;

definition
let T be TopSpace;
let F be Subset-Family of T;
func Fr F ->  Subset-Family of T means :Def1: :: TOPGEN_1:def 1
 for A being Subset of T holds
( A in it iff ex B being Subset of T st
( A = Fr B & B in F ) );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Fr B & B in F ) )
proof
defpred S1[ set ] means  ex W being Subset of T st
( $1 = Fr W & W in F );
thus  ex S being Subset-Family of T st
for Z being Subset of T holds
( Z in S iff S1[Z] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex W being Subset of T st
( $1 = Fr W & W in F );
let H, G be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) & ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) implies H = G )
assume that
A1: for Z being Subset of T holds
( Z in H iff S1[Z] ) and
A2: for X being Subset of T holds
( X in G iff S1[X] ) ; ::_thesis: H = G
now__::_thesis:_for_X_being_set_st_X_in_G_holds_
X_in_H
let X be set ; ::_thesis: ( X in G implies X in H )
assume A3: X in G ; ::_thesis: X in H
then reconsider X9 = X as Subset of T ;
 S1[X9] by A2, A3;
hence  X in H by A1; ::_thesis: verum
end;
then A4: G c= H by TARSKI:def_3;
now__::_thesis:_for_Z_being_set_st_Z_in_H_holds_
Z_in_G
let Z be set ; ::_thesis: ( Z in H implies Z in G )
assume  Z in H ; ::_thesis: Z in G
then  S1[Z] by A1;
hence  Z in G by A2; ::_thesis: verum
end;
then  H c= G by TARSKI:def_3;
hence  H = G by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Fr TOPGEN_1:def_1_:_
 for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Fr F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Fr B & B in F ) ) );

theorem :: TOPGEN_1:4
for T being TopSpace
for F being Subset-Family of T st F = {} holds
Fr F = {}
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T st F = {} holds
Fr F = {}
let F be Subset-Family of T; ::_thesis: ( F = {} implies Fr F = {} )
assume A1: F = {} ; ::_thesis: Fr F = {}
assume  Fr F <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in Fr F by XBOOLE_0:def_1;
 ex B being Subset of T st
( x = Fr B & B in F ) by A2, Def1;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: TOPGEN_1:5
for T being TopSpace
for F being Subset-Family of T
for A being Subset of T st F = {A} holds
Fr F = {(Fr A)}
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T
for A being Subset of T st F = {A} holds
Fr F = {(Fr A)}
let F be Subset-Family of T; ::_thesis: for A being Subset of T st F = {A} holds
Fr F = {(Fr A)}
let A be Subset of T; ::_thesis: ( F = {A} implies Fr F = {(Fr A)} )
assume A1: F = {A} ; ::_thesis: Fr F = {(Fr A)}
thus  Fr F c= {(Fr A)} :: according to XBOOLE_0:def_10 ::_thesis: {(Fr A)} c= Fr F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr F or x in {(Fr A)} )
assume A2: x in Fr F ; ::_thesis: x in {(Fr A)}
then reconsider B = x as Subset of T ;
consider C being Subset of T such that
A3: B = Fr C and
A4: C in F by A2, Def1;
 C = A by A1, A4, TARSKI:def_1;
hence  x in {(Fr A)} by A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Fr A)} or x in Fr F )
assume  x in {(Fr A)} ; ::_thesis: x in Fr F
then A5: x = Fr A by TARSKI:def_1;
 A in F by A1, TARSKI:def_1;
hence  x in Fr F by A5, Def1; ::_thesis: verum
end;

theorem Th6: :: TOPGEN_1:6
for T being TopSpace
for F, G being Subset-Family of T st F c= G holds
Fr F c= Fr G
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T st F c= G holds
Fr F c= Fr G
let F, G be Subset-Family of T; ::_thesis: ( F c= G implies Fr F c= Fr G )
assume A1: F c= G ; ::_thesis: Fr F c= Fr G
 Fr F c= Fr G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr F or x in Fr G )
assume A2: x in Fr F ; ::_thesis: x in Fr G
then reconsider A = x as Subset of T ;
 ex B being Subset of T st
( A = Fr B & B in F ) by A2, Def1;
hence  x in Fr G by A1, Def1; ::_thesis: verum
end;
hence  Fr F c= Fr G ; ::_thesis: verum
end;

theorem :: TOPGEN_1:7
for T being TopSpace
for F, G being Subset-Family of T holds Fr (F \/ G) = (Fr F) \/ (Fr G)
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Fr (F \/ G) = (Fr F) \/ (Fr G)
let F, G be Subset-Family of T; ::_thesis: Fr (F \/ G) = (Fr F) \/ (Fr G)
thus  Fr (F \/ G) c= (Fr F) \/ (Fr G) :: according to XBOOLE_0:def_10 ::_thesis: (Fr F) \/ (Fr G) c= Fr (F \/ G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (F \/ G) or x in (Fr F) \/ (Fr G) )
assume A1: x in Fr (F \/ G) ; ::_thesis: x in (Fr F) \/ (Fr G)
then reconsider A = x as Subset of T ;
consider B being Subset of T such that
A2: A = Fr B and
A3: B in F \/ G by A1, Def1;
percases ( B in F or B in G ) by A3, XBOOLE_0:def_3;
suppose B in F ; ::_thesis: x in (Fr F) \/ (Fr G)
then  A in Fr F by A2, Def1;
hence  x in (Fr F) \/ (Fr G) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose B in G ; ::_thesis: x in (Fr F) \/ (Fr G)
then  A in Fr G by A2, Def1;
hence  x in (Fr F) \/ (Fr G) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
 ( Fr F c= Fr (F \/ G) & Fr G c= Fr (F \/ G) ) by Th6, XBOOLE_1:7;
hence  (Fr F) \/ (Fr G) c= Fr (F \/ G) by XBOOLE_1:8; ::_thesis: verum
end;

theorem Th8: :: TOPGEN_1:8
for T being TopStruct
for A being Subset of T holds Fr A = (Cl A) \ (Int A)
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds Fr A = (Cl A) \ (Int A)
let A be Subset of T; ::_thesis: Fr A = (Cl A) \ (Int A)
Fr A = (Cl A) /\ (((Cl (A `)) `) `) by TOPS_1:def_2
.= (Cl A) \ ((Cl (A `)) `) by SUBSET_1:13
.= (Cl A) \ (Int A) by TOPS_1:def_1 ;
hence  Fr A = (Cl A) \ (Int A) ; ::_thesis: verum
end;

theorem Th9: :: TOPGEN_1:9
for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being Point of T holds
( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )
let A be Subset of T; ::_thesis: for p being Point of T holds
( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )
let p be Point of T; ::_thesis: ( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )
hereby  ::_thesis: ( ( for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) ) implies p in Fr A )
assume A1: p in Fr A ; ::_thesis: for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} )
let U be Subset of T; ::_thesis: ( U is open & p in U implies ( A meets U & U \ A <> {} ) )
assume A2: ( U is open & p in U ) ; ::_thesis: ( A meets U & U \ A <> {} )
then  U meets A ` by A1, TOPS_1:28;
hence  ( A meets U & U \ A <> {} ) by A1, A2, Th1, TOPS_1:28; ::_thesis: verum
end;
assume A3: for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) ; ::_thesis: p in Fr A
 for U being Subset of T st U is open & p in U holds
( A meets U & U meets A ` )
proof
let U be Subset of T; ::_thesis: ( U is open & p in U implies ( A meets U & U meets A ` ) )
assume A4: ( U is open & p in U ) ; ::_thesis: ( A meets U & U meets A ` )
then  U \ A <> {} by A3;
hence  ( A meets U & U meets A ` ) by A3, A4, Th1; ::_thesis: verum
end;
hence  p in Fr A by TOPS_1:28; ::_thesis: verum
end;

theorem :: TOPGEN_1:10
for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being Point of T holds
( p in Fr A iff for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
let A be Subset of T; ::_thesis: for p being Point of T holds
( p in Fr A iff for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
let p be Point of T; ::_thesis: ( p in Fr A iff for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
hereby  ::_thesis: ( ( for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) ) implies p in Fr A )
assume A1: p in Fr A ; ::_thesis: for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} )
let B be Basis of ; ::_thesis: for U being Subset of T st U in B holds
( A meets U & U \ A <> {} )
let U be Subset of T; ::_thesis: ( U in B implies ( A meets U & U \ A <> {} ) )
assume  U in B ; ::_thesis: ( A meets U & U \ A <> {} )
then  ( U is open & p in U ) by YELLOW_8:12;
hence  ( A meets U & U \ A <> {} ) by A1, Th9; ::_thesis: verum
end;
assume A2: for B being Basis of
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) ; ::_thesis: p in Fr A
 for U being Subset of T st U is open & p in U holds
( A meets U & U meets A ` )
proof
set B = the Basis of ;
let U be Subset of T; ::_thesis: ( U is open & p in U implies ( A meets U & U meets A ` ) )
assume  ( U is open & p in U ) ; ::_thesis: ( A meets U & U meets A ` )
then consider V being Subset of T such that
A3: V in the Basis of and
A4: V c= U by YELLOW_8:def_1;
 V \ A <> {} by A2, A3;
then A5: U \ A <> {} by A4, XBOOLE_1:3, XBOOLE_1:33;
 A meets V by A2, A3;
hence  ( A meets U & U meets A ` ) by A4, A5, Th1, XBOOLE_1:63; ::_thesis: verum
end;
hence  p in Fr A by TOPS_1:28; ::_thesis: verum
end;

theorem :: TOPGEN_1:11
for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being Point of T holds
( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
let A be Subset of T; ::_thesis: for p being Point of T holds
( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
let p be Point of T; ::_thesis: ( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
hereby  ::_thesis: ( ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) implies p in Fr A )
set B = the Basis of ;
assume A1: p in Fr A ; ::_thesis: ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} )
take B = the Basis of ; ::_thesis: for U being Subset of T st U in B holds
( A meets U & U \ A <> {} )
let U be Subset of T; ::_thesis: ( U in B implies ( A meets U & U \ A <> {} ) )
assume  U in B ; ::_thesis: ( A meets U & U \ A <> {} )
then  ( U is open & p in U ) by YELLOW_8:12;
hence  ( A meets U & U \ A <> {} ) by A1, Th9; ::_thesis: verum
end;
given B being Basis of  such that A2: for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) ; ::_thesis: p in Fr A
 for U being Subset of T st U is open & p in U holds
( A meets U & U meets A ` )
proof
let U be Subset of T; ::_thesis: ( U is open & p in U implies ( A meets U & U meets A ` ) )
assume  ( U is open & p in U ) ; ::_thesis: ( A meets U & U meets A ` )
then consider V being Subset of T such that
A3: V in B and
A4: V c= U by YELLOW_8:def_1;
 V \ A <> {} by A2, A3;
then A5: U \ A <> {} by A4, XBOOLE_1:3, XBOOLE_1:33;
 A meets V by A2, A3;
hence  ( A meets U & U meets A ` ) by A4, A5, Th1, XBOOLE_1:63; ::_thesis: verum
end;
hence  p in Fr A by TOPS_1:28; ::_thesis: verum
end;

theorem :: TOPGEN_1:12
for T being TopSpace
for A, B being Subset of T holds Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B))
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B))
let A, B be Subset of T; ::_thesis: Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B))
A1: ((Cl A) /\ (Cl B)) /\ ((Cl (A `)) \/ (Cl (B `))) = (((Cl A) /\ (Cl B)) /\ (Cl (A `))) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B `))) by XBOOLE_1:23
.= (((Cl A) /\ (Cl (A `))) /\ (Cl B)) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B `))) by XBOOLE_1:16
.= ((Fr A) /\ (Cl B)) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B `))) by TOPS_1:def_2
.= ((Fr A) /\ (Cl B)) \/ ((Cl A) /\ ((Cl B) /\ (Cl (B `)))) by XBOOLE_1:16
.= ((Fr A) /\ (Cl B)) \/ ((Cl A) /\ (Fr B)) by TOPS_1:def_2 ;
Fr (A /\ B) = (Cl (A /\ B)) /\ (Cl ((A /\ B) `)) by TOPS_1:def_2
.= (Cl (A /\ B)) /\ (Cl ((A `) \/ (B `))) by XBOOLE_1:54
.= (Cl (A /\ B)) /\ ((Cl (A `)) \/ (Cl (B `))) by PRE_TOPC:20 ;
hence  Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B)) by A1, PRE_TOPC:21, XBOOLE_1:26; ::_thesis: verum
end;

theorem :: TOPGEN_1:13
for T being TopSpace
for A being Subset of T holds the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A `))
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A `))
let A be Subset of T; ::_thesis: the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A `))
((Int A) \/ (Fr A)) \/ (Int (A `)) = ((Int A) \/ (Int (A `))) \/ (Fr A) by XBOOLE_1:4
.= ((Int A) \/ (Int (A `))) \/ ((Cl A) /\ (Cl (A `))) by TOPS_1:def_2
.= (((Int A) \/ (Int (A `))) \/ (Cl A)) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) by XBOOLE_1:24
.= (((Int A) \/ ((Cl A) `)) \/ (Cl A)) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) by TDLAT_3:3
.= ((Int A) \/ (((Cl A) `) \/ (Cl A))) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) by XBOOLE_1:4
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) by PRE_TOPC:2
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ (Int (A `))) \/ ((Int A) `)) by TDLAT_3:2
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ ((Int A) `)) \/ (Int (A `))) by XBOOLE_1:4
.= ((Int A) \/ ([#] T)) /\ (([#] T) \/ (Int (A `))) by PRE_TOPC:2
.= ([#] T) /\ (([#] T) \/ (Int (A `))) by XBOOLE_1:12
.= ([#] T) /\ ([#] T) by XBOOLE_1:12
.= [#] T ;
hence  the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A `)) ; ::_thesis: verum
end;

theorem Th14: :: TOPGEN_1:14
for T being TopSpace
for A being Subset of T holds
( ( A is open & A is closed ) iff Fr A = {} )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( ( A is open & A is closed ) iff Fr A = {} )
let A be Subset of T; ::_thesis: ( ( A is open & A is closed ) iff Fr A = {} )
hereby  ::_thesis: ( Fr A = {} implies ( A is open & A is closed ) )
assume A1: ( A is open & A is closed ) ; ::_thesis: Fr A = {}
then A2: Int A = A by TOPS_1:23;
Fr A = A \ (Int A) by A1, TOPS_1:43
.= {} by A2, XBOOLE_1:37 ;
hence  Fr A = {} ; ::_thesis: verum
end;
assume A3: Fr A = {} ; ::_thesis: ( A is open & A is closed )
 Fr A = (Cl A) \ (Int A) by Th8;
then A4: Cl A c= Int A by A3, XBOOLE_1:37;
A5: Int A c= A by TOPS_1:16;
then  ( A c= Cl A & Cl A c= A ) by A4, PRE_TOPC:18, XBOOLE_1:1;
then  Cl A = A by XBOOLE_0:def_10;
hence  ( A is open & A is closed ) by A4, A5, XBOOLE_0:def_10; ::_thesis: verum
end;

begin

definition
let T be TopStruct ;
let A be Subset of T;
let x be set ;
predx is_an_accumulation_point_of A means :Def2: :: TOPGEN_1:def 2
x in Cl (A \ {x});
end;

:: deftheorem Def2 defines is_an_accumulation_point_of TOPGEN_1:def_2_:_
 for T being TopStruct
for A being Subset of T
for x being set holds
( x is_an_accumulation_point_of A iff x in Cl (A \ {x}) );

theorem Th15: :: TOPGEN_1:15
for T being TopSpace
for A being Subset of T
for x being set st x is_an_accumulation_point_of A holds
x is Point of T
proof
let T be TopSpace; ::_thesis: for A being Subset of T
for x being set st x is_an_accumulation_point_of A holds
x is Point of T
let A be Subset of T; ::_thesis: for x being set st x is_an_accumulation_point_of A holds
x is Point of T
let x be set ; ::_thesis: ( x is_an_accumulation_point_of A implies x is Point of T )
assume  x is_an_accumulation_point_of A ; ::_thesis: x is Point of T
then  x in Cl (A \ {x}) by Def2;
hence  x is Point of T ; ::_thesis: verum
end;

definition
let T be TopStruct ;
let A be Subset of T;
func Der A ->  Subset of T means :Def3: :: TOPGEN_1:def 3
 for x being set st x in the carrier of T holds
( x in it iff x is_an_accumulation_point_of A );
existence
 ex b1 being Subset of T st
for x being set st x in the carrier of T holds
( x in b1 iff x is_an_accumulation_point_of A )
proof
defpred S1[ set ] means $1 is_an_accumulation_point_of A;
consider D being Subset of T such that
A1: for x being set holds
( x in D iff ( x in the carrier of T & S1[x] ) ) from SUBSET_1:sch_1();
take  D ; ::_thesis: for x being set st x in the carrier of T holds
( x in D iff x is_an_accumulation_point_of A )
thus  for x being set st x in the carrier of T holds
( x in D iff x is_an_accumulation_point_of A ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of T st ( for x being set st x in the carrier of T holds
( x in b1 iff x is_an_accumulation_point_of A ) ) & ( for x being set st x in the carrier of T holds
( x in b2 iff x is_an_accumulation_point_of A ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is_an_accumulation_point_of A;
let A1, A2 be Subset of T; ::_thesis: ( ( for x being set st x in the carrier of T holds
( x in A1 iff x is_an_accumulation_point_of A ) ) & ( for x being set st x in the carrier of T holds
( x in A2 iff x is_an_accumulation_point_of A ) ) implies A1 = A2 )
assume that
A2: for x being set st x in the carrier of T holds
( x in A1 iff S1[x] ) and
A3: for x being set st x in the carrier of T holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
A4: A2 c= A1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A2 or x in A1 )
assume A5: x in A2 ; ::_thesis: x in A1
then  S1[x] by A3;
hence  x in A1 by A2, A5; ::_thesis: verum
end;
 A1 c= A2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in A2 )
assume A6: x in A1 ; ::_thesis: x in A2
then  S1[x] by A2;
hence  x in A2 by A3, A6; ::_thesis: verum
end;
hence  A1 = A2 by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Der TOPGEN_1:def_3_:_
 for T being TopStruct
for A, b3 being Subset of T holds
( b3 = Der A iff for x being set st x in the carrier of T holds
( x in b3 iff x is_an_accumulation_point_of A ) );

theorem Th16: :: TOPGEN_1:16
for T being non empty TopSpace
for A being Subset of T
for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )
let A be Subset of T; ::_thesis: for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )
let x be set ; ::_thesis: ( x in Der A iff x is_an_accumulation_point_of A )
thus  ( x in Der A implies x is_an_accumulation_point_of A ) by Def3; ::_thesis: ( x is_an_accumulation_point_of A implies x in Der A )
assume A1: x is_an_accumulation_point_of A ; ::_thesis: x in Der A
then  x is Point of T by Th15;
hence  x in Der A by A1, Def3; ::_thesis: verum
end;

theorem Th17: :: TOPGEN_1:17
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Der A iff for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Point of T holds
( x in Der A iff for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let A be Subset of T; ::_thesis: for x being Point of T holds
( x in Der A iff for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let x be Point of T; ::_thesis: ( x in Der A iff for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
hereby  ::_thesis: ( ( for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) ) implies x in Der A )
assume  x in Der A ; ::_thesis: for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y )
then  x is_an_accumulation_point_of A by Th16;
then A1: x in Cl (A \ {x}) by Def2;
let U be open Subset of T; ::_thesis: ( x in U implies ex y being Point of T st
( y in A /\ U & x <> y ) )
assume  x in U ; ::_thesis: ex y being Point of T st
( y in A /\ U & x <> y )
then  A \ {x} meets U by A1, PRE_TOPC:24;
then consider y being set  such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y = y as Point of T by A2;
take y = y; ::_thesis: ( y in A /\ U & x <> y )
 y in A by A2, ZFMISC_1:56;
hence  ( y in A /\ U & x <> y ) by A2, A3, XBOOLE_0:def_4, ZFMISC_1:56; ::_thesis: verum
end;
assume A4: for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) ; ::_thesis: x in Der A
 for G being Subset of T st G is open & x in G holds
A \ {x} meets G
proof
let G be Subset of T; ::_thesis: ( G is open & x in G implies A \ {x} meets G )
assume A5: G is open ; ::_thesis: ( not x in G or A \ {x} meets G )
assume  x in G ; ::_thesis: A \ {x} meets G
then consider y being Point of T such that
A6: y in A /\ G and
A7: x <> y by A4, A5;
 y in A by A6, XBOOLE_0:def_4;
then A8: y in A \ {x} by A7, ZFMISC_1:56;
 y in G by A6, XBOOLE_0:def_4;
hence  A \ {x} meets G by A8, XBOOLE_0:3; ::_thesis: verum
end;
then  x in Cl (A \ {x}) by PRE_TOPC:24;
then  x is_an_accumulation_point_of A by Def2;
hence  x in Der A by Th16; ::_thesis: verum
end;

theorem :: TOPGEN_1:18
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Point of T holds
( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let A be Subset of T; ::_thesis: for x being Point of T holds
( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let x be Point of T; ::_thesis: ( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
hereby  ::_thesis: ( ( for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) ) implies x in Der A )
assume  x in Der A ; ::_thesis: for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y )
then  x is_an_accumulation_point_of A by Th16;
then A1: x in Cl (A \ {x}) by Def2;
let B be Basis of ; ::_thesis: for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y )
let U be Subset of T; ::_thesis: ( U in B implies ex y being Point of T st
( y in A /\ U & x <> y ) )
assume  U in B ; ::_thesis: ex y being Point of T st
( y in A /\ U & x <> y )
then  ( U is open & x in U ) by YELLOW_8:12;
then  A \ {x} meets U by A1, PRE_TOPC:24;
then consider y being set  such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y = y as Point of T by A2;
take y = y; ::_thesis: ( y in A /\ U & x <> y )
 y in A by A2, ZFMISC_1:56;
hence  ( y in A /\ U & x <> y ) by A2, A3, XBOOLE_0:def_4, ZFMISC_1:56; ::_thesis: verum
end;
assume A4: for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) ; ::_thesis: x in Der A
 for G being Subset of T st G is open & x in G holds
A \ {x} meets G
proof
set B = the Basis of ;
let G be Subset of T; ::_thesis: ( G is open & x in G implies A \ {x} meets G )
assume A5: G is open ; ::_thesis: ( not x in G or A \ {x} meets G )
assume  x in G ; ::_thesis: A \ {x} meets G
then consider V being Subset of T such that
A6: ( V in the Basis of & V c= G ) by A5, YELLOW_8:13;
 ( ex y being Point of T st
( y in A /\ V & x <> y ) & A /\ V c= A /\ G ) by A4, A6, XBOOLE_1:26;
then consider y being Point of T such that
A7: y in A /\ G and
A8: x <> y ;
 y in A by A7, XBOOLE_0:def_4;
then A9: y in A \ {x} by A8, ZFMISC_1:56;
 y in G by A7, XBOOLE_0:def_4;
hence  A \ {x} meets G by A9, XBOOLE_0:3; ::_thesis: verum
end;
then  x in Cl (A \ {x}) by PRE_TOPC:24;
then  x is_an_accumulation_point_of A by Def2;
hence  x in Der A by Th16; ::_thesis: verum
end;

theorem :: TOPGEN_1:19
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Der A iff ex B being Basis of st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Point of T holds
( x in Der A iff ex B being Basis of st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let A be Subset of T; ::_thesis: for x being Point of T holds
( x in Der A iff ex B being Basis of st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let x be Point of T; ::_thesis: ( x in Der A iff ex B being Basis of st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
hereby  ::_thesis: ( ex B being Basis of st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) implies x in Der A )
set B = the Basis of ;
assume  x in Der A ; ::_thesis: ex B being Basis of st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y )
then  x is_an_accumulation_point_of A by Th16;
then A1: x in Cl (A \ {x}) by Def2;
take B = the Basis of ; ::_thesis: for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y )
let U be Subset of T; ::_thesis: ( U in B implies ex y being Point of T st
( y in A /\ U & x <> y ) )
assume  U in B ; ::_thesis: ex y being Point of T st
( y in A /\ U & x <> y )
then  ( U is open & x in U ) by YELLOW_8:12;
then  A \ {x} meets U by A1, PRE_TOPC:24;
then consider y being set  such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y = y as Point of T by A2;
take y = y; ::_thesis: ( y in A /\ U & x <> y )
 y in A by A2, ZFMISC_1:56;
hence  ( y in A /\ U & x <> y ) by A2, A3, XBOOLE_0:def_4, ZFMISC_1:56; ::_thesis: verum
end;
given B being Basis of  such that A4: for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) ; ::_thesis: x in Der A
 for G being Subset of T st G is open & x in G holds
A \ {x} meets G
proof
let G be Subset of T; ::_thesis: ( G is open & x in G implies A \ {x} meets G )
assume A5: G is open ; ::_thesis: ( not x in G or A \ {x} meets G )
assume  x in G ; ::_thesis: A \ {x} meets G
then consider V being Subset of T such that
A6: ( V in B & V c= G ) by A5, YELLOW_8:13;
 ( ex y being Point of T st
( y in A /\ V & x <> y ) & A /\ V c= A /\ G ) by A4, A6, XBOOLE_1:26;
then consider y being Point of T such that
A7: y in A /\ G and
A8: x <> y ;
 y in A by A7, XBOOLE_0:def_4;
then A9: y in A \ {x} by A8, ZFMISC_1:56;
 y in G by A7, XBOOLE_0:def_4;
hence  A \ {x} meets G by A9, XBOOLE_0:3; ::_thesis: verum
end;
then  x in Cl (A \ {x}) by PRE_TOPC:24;
then  x is_an_accumulation_point_of A by Def2;
hence  x in Der A by Th16; ::_thesis: verum
end;

begin

definition
let T be TopSpace;
let A be Subset of T;
let x be set ;
predx is_isolated_in A means :Def4: :: TOPGEN_1:def 4
( x in A & not x is_an_accumulation_point_of A );
end;

:: deftheorem Def4 defines is_isolated_in TOPGEN_1:def_4_:_
 for T being TopSpace
for A being Subset of T
for x being set holds
( x is_isolated_in A iff ( x in A & not x is_an_accumulation_point_of A ) );

theorem :: TOPGEN_1:20
for T being non empty TopSpace
for A being Subset of T
for p being set holds
( p in A \ (Der A) iff p is_isolated_in A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being set holds
( p in A \ (Der A) iff p is_isolated_in A )
let A be Subset of T; ::_thesis: for p being set holds
( p in A \ (Der A) iff p is_isolated_in A )
let p be set ; ::_thesis: ( p in A \ (Der A) iff p is_isolated_in A )
hereby  ::_thesis: ( p is_isolated_in A implies p in A \ (Der A) )
assume A1: p in A \ (Der A) ; ::_thesis: p is_isolated_in A
then  not p in Der A by XBOOLE_0:def_5;
then A2: not p is_an_accumulation_point_of A by Th16;
 p in A by A1, XBOOLE_0:def_5;
hence  p is_isolated_in A by A2, Def4; ::_thesis: verum
end;
assume A3: p is_isolated_in A ; ::_thesis: p in A \ (Der A)
then  not p is_an_accumulation_point_of A by Def4;
then A4: not p in Der A by Th16;
 p in A by A3, Def4;
hence  p in A \ (Der A) by A4, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th21: :: TOPGEN_1:21
for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p is_an_accumulation_point_of A iff for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being Point of T holds
( p is_an_accumulation_point_of A iff for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) )
let A be Subset of T; ::_thesis: for p being Point of T holds
( p is_an_accumulation_point_of A iff for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) )
let p be Point of T; ::_thesis: ( p is_an_accumulation_point_of A iff for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) )
hereby  ::_thesis: ( ( for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) ) implies p is_an_accumulation_point_of A )
assume  p is_an_accumulation_point_of A ; ::_thesis: for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U )
then A1: p in Der A by Th16;
let U be open Subset of T; ::_thesis: ( p in U implies ex q being Point of T st
( q <> p & q in A & q in U ) )
assume  p in U ; ::_thesis: ex q being Point of T st
( q <> p & q in A & q in U )
then consider q being Point of T such that
A2: ( q in A /\ U & p <> q ) by A1, Th17;
take q = q; ::_thesis: ( q <> p & q in A & q in U )
thus  ( q <> p & q in A & q in U ) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) ; ::_thesis: p is_an_accumulation_point_of A
 for U being open Subset of T st p in U holds
ex y being Point of T st
( y in A /\ U & p <> y )
proof
let U be open Subset of T; ::_thesis: ( p in U implies ex y being Point of T st
( y in A /\ U & p <> y ) )
assume  p in U ; ::_thesis: ex y being Point of T st
( y in A /\ U & p <> y )
then consider q being Point of T such that
A4: ( q <> p & q in A & q in U ) by A3;
take  q ; ::_thesis: ( q in A /\ U & p <> q )
thus  ( q in A /\ U & p <> q ) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
then  p in Der A by Th17;
hence  p is_an_accumulation_point_of A by Th16; ::_thesis: verum
end;

theorem Th22: :: TOPGEN_1:22
for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being Point of T holds
( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )
let A be Subset of T; ::_thesis: for p being Point of T holds
( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )
let p be Point of T; ::_thesis: ( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )
hereby  ::_thesis: ( ex G being open Subset of T st G /\ A = {p} implies p is_isolated_in A )
assume A1: p is_isolated_in A ; ::_thesis: ex U being open Subset of T st U /\ A = {p}
then  not p is_an_accumulation_point_of A by Def4;
then consider U being open Subset of T such that
A2: p in U and
A3: for q being Point of T holds
( not q <> p or not q in A or not q in U ) by Th21;
take U = U; ::_thesis: U /\ A = {p}
A4: p in A by A1, Def4;
 U /\ A = {p}
proof
thus  U /\ A c= {p} :: according to XBOOLE_0:def_10 ::_thesis: {p} c= U /\ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U /\ A or x in {p} )
assume  x in U /\ A ; ::_thesis: x in {p}
then  ( x in U & x in A ) by XBOOLE_0:def_4;
then  x = p by A3;
hence  x in {p} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p} or x in U /\ A )
assume  x in {p} ; ::_thesis: x in U /\ A
then  x = p by TARSKI:def_1;
hence  x in U /\ A by A4, A2, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  U /\ A = {p} ; ::_thesis: verum
end;
given G being open Subset of T such that A5: G /\ A = {p} ; ::_thesis: p is_isolated_in A
A6: p in G /\ A by A5, TARSKI:def_1;
 ex U being open Subset of T st
( p in U & ( for q being Point of T holds
( not q <> p or not q in A or not q in U ) ) )
proof
take  G ; ::_thesis: ( p in G & ( for q being Point of T holds
( not q <> p or not q in A or not q in G ) ) )
 for q being Point of T holds
( q = p or not q in A or not q in G )
proof
given q being Point of T such that A7: q <> p and
A8: ( q in A & q in G ) ; ::_thesis: contradiction
 q in A /\ G by A8, XBOOLE_0:def_4;
hence  contradiction by A5, A7, TARSKI:def_1; ::_thesis: verum
end;
hence  ( p in G & ( for q being Point of T holds
( not q <> p or not q in A or not q in G ) ) ) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A9: not p is_an_accumulation_point_of A by Th21;
 p in A by A6, XBOOLE_0:def_4;
hence  p is_isolated_in A by A9, Def4; ::_thesis: verum
end;

definition
let T be TopSpace;
let p be Point of T;
attrp is isolated  means :Def5: :: TOPGEN_1:def 5
p is_isolated_in [#] T;
end;

:: deftheorem Def5 defines isolated TOPGEN_1:def_5_:_
 for T being TopSpace
for p being Point of T holds
( p is isolated iff p is_isolated_in [#] T );

theorem :: TOPGEN_1:23
for T being non empty TopSpace
for p being Point of T holds
( p is isolated iff {p} is open )
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds
( p is isolated iff {p} is open )
let p be Point of T; ::_thesis: ( p is isolated iff {p} is open )
A1: {p} /\ ([#] T) = {p} by XBOOLE_1:28;
hereby  ::_thesis: ( {p} is open implies p is isolated )
assume  p is isolated ; ::_thesis: {p} is open
then  p is_isolated_in [#] T by Def5;
then  ex G being open Subset of T st G /\ ([#] T) = {p} by Th22;
hence  {p} is open ; ::_thesis: verum
end;
assume  {p} is open ; ::_thesis: p is isolated
then  p is_isolated_in [#] T by A1, Th22;
hence  p is isolated by Def5; ::_thesis: verum
end;

begin

definition
let T be TopSpace;
let F be Subset-Family of T;
func Der F ->  Subset-Family of T means :Def6: :: TOPGEN_1:def 6
 for A being Subset of T holds
( A in it iff ex B being Subset of T st
( A = Der B & B in F ) );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Der B & B in F ) )
proof
defpred S1[ set ] means  ex W being Subset of T st
( $1 = Der W & W in F );
thus  ex S being Subset-Family of T st
for Z being Subset of T holds
( Z in S iff S1[Z] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Der B & B in F ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Der B & B in F ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex W being Subset of T st
( $1 = Der W & W in F );
let H, G be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Der B & B in F ) ) ) & ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Der B & B in F ) ) ) implies H = G )
assume that
A1: for Z being Subset of T holds
( Z in H iff S1[Z] ) and
A2: for X being Subset of T holds
( X in G iff S1[X] ) ; ::_thesis: H = G
now__::_thesis:_for_X_being_set_st_X_in_G_holds_
X_in_H
let X be set ; ::_thesis: ( X in G implies X in H )
assume A3: X in G ; ::_thesis: X in H
then reconsider X9 = X as Subset of T ;
 S1[X9] by A2, A3;
hence  X in H by A1; ::_thesis: verum
end;
then A4: G c= H by TARSKI:def_3;
now__::_thesis:_for_Z_being_set_st_Z_in_H_holds_
Z_in_G
let Z be set ; ::_thesis: ( Z in H implies Z in G )
assume  Z in H ; ::_thesis: Z in G
then  S1[Z] by A1;
hence  Z in G by A2; ::_thesis: verum
end;
then  H c= G by TARSKI:def_3;
hence  H = G by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Der TOPGEN_1:def_6_:_
 for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Der F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Der B & B in F ) ) );


theorem :: TOPGEN_1:24
for T being non empty TopSpace
for F being Subset-Family of T st F = {} holds
Der F = {}
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F = {} holds
Der F = {}
let F be Subset-Family of T; ::_thesis: ( F = {} implies Der F = {} )
assume A1: F = {} ; ::_thesis: Der F = {}
assume  Der F <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in Der F by XBOOLE_0:def_1;
 ex B being Subset of T st
( x = Der B & B in F ) by A2, Def6;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: TOPGEN_1:25
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Der F = {(Der A)}
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Der F = {(Der A)}
let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds
Der F = {(Der A)}
let F be Subset-Family of T; ::_thesis: ( F = {A} implies Der F = {(Der A)} )
assume A1: F = {A} ; ::_thesis: Der F = {(Der A)}
thus  Der F c= {(Der A)} :: according to XBOOLE_0:def_10 ::_thesis: {(Der A)} c= Der F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der F or x in {(Der A)} )
assume A2: x in Der F ; ::_thesis: x in {(Der A)}
then reconsider B = x as Subset of T ;
consider C being Subset of T such that
A3: B = Der C and
A4: C in F by A2, Def6;
 C = A by A1, A4, TARSKI:def_1;
hence  x in {(Der A)} by A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Der A)} or x in Der F )
assume  x in {(Der A)} ; ::_thesis: x in Der F
then A5: x = Der A by TARSKI:def_1;
 A in F by A1, TARSKI:def_1;
hence  x in Der F by A5, Def6; ::_thesis: verum
end;

theorem Th26: :: TOPGEN_1:26
for T being non empty TopSpace
for F, G being Subset-Family of T st F c= G holds
Der F c= Der G
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F c= G holds
Der F c= Der G
let F, G be Subset-Family of T; ::_thesis: ( F c= G implies Der F c= Der G )
assume A1: F c= G ; ::_thesis: Der F c= Der G
 Der F c= Der G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der F or x in Der G )
assume A2: x in Der F ; ::_thesis: x in Der G
then reconsider A = x as Subset of T ;
 ex B being Subset of T st
( A = Der B & B in F ) by A2, Def6;
hence  x in Der G by A1, Def6; ::_thesis: verum
end;
hence  Der F c= Der G ; ::_thesis: verum
end;

theorem :: TOPGEN_1:27
for T being non empty TopSpace
for F, G being Subset-Family of T holds Der (F \/ G) = (Der F) \/ (Der G)
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T holds Der (F \/ G) = (Der F) \/ (Der G)
let F, G be Subset-Family of T; ::_thesis: Der (F \/ G) = (Der F) \/ (Der G)
thus  Der (F \/ G) c= (Der F) \/ (Der G) :: according to XBOOLE_0:def_10 ::_thesis: (Der F) \/ (Der G) c= Der (F \/ G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der (F \/ G) or x in (Der F) \/ (Der G) )
assume A1: x in Der (F \/ G) ; ::_thesis: x in (Der F) \/ (Der G)
then reconsider A = x as Subset of T ;
consider B being Subset of T such that
A2: A = Der B and
A3: B in F \/ G by A1, Def6;
percases ( B in F or B in G ) by A3, XBOOLE_0:def_3;
suppose B in F ; ::_thesis: x in (Der F) \/ (Der G)
then  A in Der F by A2, Def6;
hence  x in (Der F) \/ (Der G) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose B in G ; ::_thesis: x in (Der F) \/ (Der G)
then  A in Der G by A2, Def6;
hence  x in (Der F) \/ (Der G) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
 ( Der F c= Der (F \/ G) & Der G c= Der (F \/ G) ) by Th26, XBOOLE_1:7;
hence  (Der F) \/ (Der G) c= Der (F \/ G) by XBOOLE_1:8; ::_thesis: verum
end;

theorem Th28: :: TOPGEN_1:28
for T being non empty TopSpace
for A being Subset of T holds Der A c= Cl A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds Der A c= Cl A
let A be Subset of T; ::_thesis: Der A c= Cl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der A or x in Cl A )
assume A1: x in Der A ; ::_thesis: x in Cl A
then reconsider x9 = x as Point of T ;
 for G being Subset of T st G is open & x9 in G holds
A meets G
proof
let G be Subset of T; ::_thesis: ( G is open & x9 in G implies A meets G )
assume A2: G is open ; ::_thesis: ( not x9 in G or A meets G )
assume  x9 in G ; ::_thesis: A meets G
then  ex y being Point of T st
( y in A /\ G & x <> y ) by A1, A2, Th17;
hence  A meets G by XBOOLE_0:4; ::_thesis: verum
end;
hence  x in Cl A by PRE_TOPC:24; ::_thesis: verum
end;

theorem Th29: :: TOPGEN_1:29
for T being TopSpace
for A being Subset of T holds Cl A = A \/ (Der A)
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Cl A = A \/ (Der A)
let A be Subset of T; ::_thesis: Cl A = A \/ (Der A)
percases ( not T is empty or T is empty ) ;
supposeA1: not T is empty ; ::_thesis: Cl A = A \/ (Der A)
then A2: Der A c= Cl A by Th28;
thus  Cl A c= A \/ (Der A) :: according to XBOOLE_0:def_10 ::_thesis: A \/ (Der A) c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A \/ (Der A) )
assume A3: x in Cl A ; ::_thesis: x in A \/ (Der A)
then reconsider x9 = x as Point of T ;
percases ( x in A or not x in A ) ;
suppose x in A ; ::_thesis: x in A \/ (Der A)
hence  x in A \/ (Der A) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA4: not x in A ; ::_thesis: x in A \/ (Der A)
 for U being open Subset of T st x9 in U holds
ex y being Point of T st
( y in A /\ U & x9 <> y )
proof
let U be open Subset of T; ::_thesis: ( x9 in U implies ex y being Point of T st
( y in A /\ U & x9 <> y ) )
assume  x9 in U ; ::_thesis: ex y being Point of T st
( y in A /\ U & x9 <> y )
then  A meets U by A3, PRE_TOPC:24;
then consider y being set  such that
A5: y in A and
A6: y in U by XBOOLE_0:3;
reconsider y = y as Point of T by A5;
take  y ; ::_thesis: ( y in A /\ U & x9 <> y )
thus  ( y in A /\ U & x9 <> y ) by A4, A5, A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then  x9 in Der A by A1, Th17;
hence  x in A \/ (Der A) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \/ (Der A) or x in Cl A )
assume A7: x in A \/ (Der A) ; ::_thesis: x in Cl A
percases ( x in A or x in Der A ) by A7, XBOOLE_0:def_3;
supposeA8: x in A ; ::_thesis: x in Cl A
 A c= Cl A by PRE_TOPC:18;
hence  x in Cl A by A8; ::_thesis: verum
end;
suppose x in Der A ; ::_thesis: x in Cl A
hence  x in Cl A by A2; ::_thesis: verum
end;
end;
end;
supposeA9: T is empty ; ::_thesis: Cl A = A \/ (Der A)
then  the carrier of T is empty ;
then  Cl A = {} \/ {}
.= A \/ (Der A) by A9 ;
hence  Cl A = A \/ (Der A) ; ::_thesis: verum
end;
end;
end;

theorem Th30: :: TOPGEN_1:30
for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
Der A c= Der B
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A c= B holds
Der A c= Der B
let A, B be Subset of T; ::_thesis: ( A c= B implies Der A c= Der B )
assume A1: A c= B ; ::_thesis: Der A c= Der B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der A or x in Der B )
assume A2: x in Der A ; ::_thesis: x in Der B
then reconsider x9 = x as Point of T ;
 for U being open Subset of T st x9 in U holds
ex y being Point of T st
( y in B /\ U & x9 <> y )
proof
let U be open Subset of T; ::_thesis: ( x9 in U implies ex y being Point of T st
( y in B /\ U & x9 <> y ) )
assume  x9 in U ; ::_thesis: ex y being Point of T st
( y in B /\ U & x9 <> y )
then A3: ex y being Point of T st
( y in A /\ U & x9 <> y ) by A2, Th17;
 A /\ U c= B /\ U by A1, XBOOLE_1:26;
hence  ex y being Point of T st
( y in B /\ U & x9 <> y ) by A3; ::_thesis: verum
end;
hence  x in Der B by Th17; ::_thesis: verum
end;

theorem Th31: :: TOPGEN_1:31
for T being non empty TopSpace
for A, B being Subset of T holds Der (A \/ B) = (Der A) \/ (Der B)
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T holds Der (A \/ B) = (Der A) \/ (Der B)
let A, B be Subset of T; ::_thesis: Der (A \/ B) = (Der A) \/ (Der B)
thus  Der (A \/ B) c= (Der A) \/ (Der B) :: according to XBOOLE_0:def_10 ::_thesis: (Der A) \/ (Der B) c= Der (A \/ B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der (A \/ B) or x in (Der A) \/ (Der B) )
assume  x in Der (A \/ B) ; ::_thesis: x in (Der A) \/ (Der B)
then  x is_an_accumulation_point_of A \/ B by Th16;
then A1: x in Cl ((A \/ B) \ {x}) by Def2;
 (A \/ B) \ {x} = (A \ {x}) \/ (B \ {x}) by XBOOLE_1:42;
then  Cl ((A \/ B) \ {x}) = (Cl (A \ {x})) \/ (Cl (B \ {x})) by PRE_TOPC:20;
then  ( x in Cl (A \ {x}) or x in Cl (B \ {x}) ) by A1, XBOOLE_0:def_3;
then  ( x is_an_accumulation_point_of A or x is_an_accumulation_point_of B ) by Def2;
then  ( x in Der A or x in Der B ) by Th16;
hence  x in (Der A) \/ (Der B) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Der A) \/ (Der B) or x in Der (A \/ B) )
assume  x in (Der A) \/ (Der B) ; ::_thesis: x in Der (A \/ B)
then  ( x in Der A or x in Der B ) by XBOOLE_0:def_3;
then A2: ( x is_an_accumulation_point_of A or x is_an_accumulation_point_of B ) by Th16;
 x in Cl ((A \/ B) \ {x})
proof
 B \ {x} c= (A \/ B) \ {x} by XBOOLE_1:7, XBOOLE_1:33;
then A3: Cl (B \ {x}) c= Cl ((A \/ B) \ {x}) by PRE_TOPC:19;
 A \ {x} c= (A \/ B) \ {x} by XBOOLE_1:7, XBOOLE_1:33;
then A4: Cl (A \ {x}) c= Cl ((A \/ B) \ {x}) by PRE_TOPC:19;
percases ( x in Cl (A \ {x}) or x in Cl (B \ {x}) ) by A2, Def2;
suppose x in Cl (A \ {x}) ; ::_thesis: x in Cl ((A \/ B) \ {x})
hence  x in Cl ((A \/ B) \ {x}) by A4; ::_thesis: verum
end;
suppose x in Cl (B \ {x}) ; ::_thesis: x in Cl ((A \/ B) \ {x})
hence  x in Cl ((A \/ B) \ {x}) by A3; ::_thesis: verum
end;
end;
end;
then  x is_an_accumulation_point_of A \/ B by Def2;
hence  x in Der (A \/ B) by Th16; ::_thesis: verum
end;

theorem Th32: :: TOPGEN_1:32
for T being non empty TopSpace
for A being Subset of T st T is T_1 holds
Der (Der A) c= Der A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st T is T_1 holds
Der (Der A) c= Der A
let A be Subset of T; ::_thesis: ( T is T_1 implies Der (Der A) c= Der A )
assume A1: T is T_1 ; ::_thesis: Der (Der A) c= Der A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der (Der A) or x in Der A )
assume A2: x in Der (Der A) ; ::_thesis: x in Der A
then reconsider x9 = x as Point of T ;
assume  not x in Der A ; ::_thesis: contradiction
then consider G being open Subset of T such that
A3: x9 in G and
A4: for y being Point of T holds
( not y in A /\ G or not x9 <> y ) by Th17;
 Cl {x9} = {x9} by A1, YELLOW_8:26;
then A5: G \ {x9} is open by FRECHET:4;
consider y being Point of T such that
A6: y in (Der A) /\ G and
A7: x <> y by A2, A3, Th17;
 y in Der A by A6, XBOOLE_0:def_4;
then A8: y in (Der A) \ {x} by A7, ZFMISC_1:56;
 y in G by A6, XBOOLE_0:def_4;
then consider q being set  such that
A9: q in G and
A10: q in (Der A) \ {x} by A8;
reconsider q = q as Point of T by A9;
 not q in {x} by A10, XBOOLE_0:def_5;
then A11: q in G \ {x} by A9, XBOOLE_0:def_5;
set U = G \ {x9};
A12: G misses A \ {x}
proof
assume  G meets A \ {x} ; ::_thesis: contradiction
then consider g being set  such that
A13: g in G and
A14: g in A \ {x} by XBOOLE_0:3;
 g in A by A14, XBOOLE_0:def_5;
then  g in A /\ G by A13, XBOOLE_0:def_4;
then  x9 = g by A4;
hence  contradiction by A14, ZFMISC_1:56; ::_thesis: verum
end;
 q in Der A by A10, XBOOLE_0:def_5;
then consider y being Point of T such that
A15: y in A /\ (G \ {x9}) and
A16: q <> y by A11, A5, Th17;
 y in A by A15, XBOOLE_0:def_4;
then A17: y in A \ {q} by A16, ZFMISC_1:56;
 y in G \ {x9} by A15, XBOOLE_0:def_4;
then consider f being set  such that
A18: f in G \ {x9} and
A19: f in A \ {q} by A17;
 ( f <> x9 & f in A ) by A18, A19, ZFMISC_1:56;
then A20: f in A \ {x9} by ZFMISC_1:56;
 f in G by A18, ZFMISC_1:56;
hence  contradiction by A12, A20, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th33: :: TOPGEN_1:33
for T being TopSpace
for A being Subset of T st T is T_1 holds
Cl (Der A) = Der A
proof
let T be TopSpace; ::_thesis: for A being Subset of T st T is T_1 holds
Cl (Der A) = Der A
let A be Subset of T; ::_thesis: ( T is T_1 implies Cl (Der A) = Der A )
assume A1: T is T_1 ; ::_thesis: Cl (Der A) = Der A
percases ( not T is empty or T is empty ) ;
supposeA2: not T is empty ; ::_thesis: Cl (Der A) = Der A
 Cl (Der A) = (Der A) \/ (Der (Der A)) by Th29;
then A3: Cl (Der A) c= (Der A) \/ (Der A) by A1, A2, Th32, XBOOLE_1:9;
 Der A c= Cl (Der A) by PRE_TOPC:18;
hence  Cl (Der A) = Der A by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA4: T is empty ; ::_thesis: Cl (Der A) = Der A
then  Cl (Der A) = {} ;
hence  Cl (Der A) = Der A by A4; ::_thesis: verum
end;
end;
end;

registration
let T be non empty T_1 TopSpace;
let A be Subset of T;
cluster Der A ->  closed ;
coherence
 Der A is closed
proof
 Der A = Cl (Der A) by Th33;
hence  Der A is closed ; ::_thesis: verum
end;
end;

theorem Th34: :: TOPGEN_1:34
for T being non empty TopSpace
for F being Subset-Family of T holds union (Der F) c= Der (union F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Der F) c= Der (union F)
let F be Subset-Family of T; ::_thesis: union (Der F) c= Der (union F)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (Der F) or x in Der (union F) )
assume  x in union (Der F) ; ::_thesis: x in Der (union F)
then consider Y being set  such that
A1: x in Y and
A2: Y in Der F by TARSKI:def_4;
reconsider Y = Y as Subset of T by A2;
consider B being Subset of T such that
A3: Y = Der B and
A4: B in F by A2, Def6;
 Der B c= Der (union F) by A4, Th30, ZFMISC_1:74;
hence  x in Der (union F) by A1, A3; ::_thesis: verum
end;

theorem :: TOPGEN_1:35
for T being non empty TopSpace
for A, B being Subset of T
for x being set st A c= B & x is_an_accumulation_point_of A holds
x is_an_accumulation_point_of B
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T
for x being set st A c= B & x is_an_accumulation_point_of A holds
x is_an_accumulation_point_of B
let A, B be Subset of T; ::_thesis: for x being set st A c= B & x is_an_accumulation_point_of A holds
x is_an_accumulation_point_of B
let x be set ; ::_thesis: ( A c= B & x is_an_accumulation_point_of A implies x is_an_accumulation_point_of B )
assume  A c= B ; ::_thesis: ( not x is_an_accumulation_point_of A or x is_an_accumulation_point_of B )
then A1: Der A c= Der B by Th30;
assume  x is_an_accumulation_point_of A ; ::_thesis: x is_an_accumulation_point_of B
then  x in Der A by Th16;
hence  x is_an_accumulation_point_of B by A1, Th16; ::_thesis: verum
end;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA is dense-in-itself  means :Def7: :: TOPGEN_1:def 7
A c= Der A;
end;

:: deftheorem Def7 defines dense-in-itself TOPGEN_1:def_7_:_
 for T being TopSpace
for A being Subset of T holds
( A is dense-in-itself iff A c= Der A );

definition
let T be non empty TopSpace;
attrT is dense-in-itself  means :: TOPGEN_1:def 8
 [#] T is dense-in-itself ;
end;

:: deftheorem  defines dense-in-itself TOPGEN_1:def_8_:_
 for T being non empty TopSpace holds
( T is dense-in-itself iff [#] T is dense-in-itself );

theorem Th36: :: TOPGEN_1:36
for T being non empty TopSpace
for A being Subset of T st T is T_1 & A is dense-in-itself holds
Cl A is dense-in-itself
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st T is T_1 & A is dense-in-itself holds
Cl A is dense-in-itself
let A be Subset of T; ::_thesis: ( T is T_1 & A is dense-in-itself implies Cl A is dense-in-itself )
assume A1: T is T_1 ; ::_thesis: ( not A is dense-in-itself or Cl A is dense-in-itself )
assume  A is dense-in-itself ; ::_thesis: Cl A is dense-in-itself
then  A c= Der A by Def7;
then A2: Der A = A \/ (Der A) by XBOOLE_1:12
.= Cl A by Th29 ;
Der (Cl A) = Der (A \/ (Der A)) by Th29
.= (Der A) \/ (Der (Der A)) by Th31
.= Cl A by A1, A2, Th32, XBOOLE_1:12 ;
hence  Cl A is dense-in-itself by Def7; ::_thesis: verum
end;

definition
let T be TopSpace;
let F be Subset-Family of T;
attrF is dense-in-itself  means :Def9: :: TOPGEN_1:def 9
 for A being Subset of T st A in F holds
A is dense-in-itself ;
end;

:: deftheorem Def9 defines dense-in-itself TOPGEN_1:def_9_:_
 for T being TopSpace
for F being Subset-Family of T holds
( F is dense-in-itself iff for A being Subset of T st A in F holds
A is dense-in-itself );

theorem Th37: :: TOPGEN_1:37
for T being non empty TopSpace
for F being Subset-Family of T st F is dense-in-itself holds
union F c= union (Der F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is dense-in-itself holds
union F c= union (Der F)
let F be Subset-Family of T; ::_thesis: ( F is dense-in-itself implies union F c= union (Der F) )
assume A1: F is dense-in-itself ; ::_thesis: union F c= union (Der F)
thus  union F c= union (Der F) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in union (Der F) )
assume  x in union F ; ::_thesis: x in union (Der F)
then consider A being set  such that
A2: x in A and
A3: A in F by TARSKI:def_4;
reconsider A = A as Subset of T by A3;
 A is dense-in-itself by A1, A3, Def9;
then A4: A c= Der A by Def7;
 Der A in Der F by A3, Def6;
hence  x in union (Der F) by A2, A4, TARSKI:def_4; ::_thesis: verum
end;
end;

theorem Th38: :: TOPGEN_1:38
for T being non empty TopSpace
for F being Subset-Family of T st F is dense-in-itself holds
union F is dense-in-itself
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is dense-in-itself holds
union F is dense-in-itself
let F be Subset-Family of T; ::_thesis: ( F is dense-in-itself implies union F is dense-in-itself )
assume  F is dense-in-itself ; ::_thesis: union F is dense-in-itself
then A1: union F c= union (Der F) by Th37;
 union (Der F) c= Der (union F) by Th34;
then  union F c= Der (union F) by A1, XBOOLE_1:1;
hence  union F is dense-in-itself by Def7; ::_thesis: verum
end;

theorem :: TOPGEN_1:39
for T being non empty TopSpace holds Fr ({} T) = {}
proof
let T be non empty TopSpace; ::_thesis: Fr ({} T) = {}
Fr ({} T) = (Cl ({} T)) /\ (Cl (({} T) `)) by TOPS_1:def_2
.= {} /\ (Cl (({} T) `)) ;
hence  Fr ({} T) = {} ; ::_thesis: verum
end;

registration
let T be TopSpace;
let A be open closed Subset of T;
cluster Fr A ->  empty ;
coherence
 Fr A is empty by Th14;
end;

registration
let T be non empty non discrete TopSpace;
cluster non open for Element of K10( the carrier of T);
existence
 not for b1 being Subset of T holds b1 is open by TDLAT_3:15;
cluster non closed for Element of K10( the carrier of T);
existence
 not for b1 being Subset of T holds b1 is closed by TDLAT_3:16;
end;

registration
let T be non empty non discrete TopSpace;
let A be non open Subset of T;
cluster Fr A ->  non empty ;
coherence
 not Fr A is empty by Th14;
end;

registration
let T be non empty non discrete TopSpace;
let A be non closed Subset of T;
cluster Fr A ->  non empty ;
coherence
 not Fr A is empty by Th14;
end;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA is perfect  means :Def10: :: TOPGEN_1:def 10
( A is closed & A is dense-in-itself );
end;

:: deftheorem Def10 defines perfect TOPGEN_1:def_10_:_
 for T being TopSpace
for A being Subset of T holds
( A is perfect iff ( A is closed & A is dense-in-itself ) );

registration
let T be TopSpace;
cluster perfect  ->  closed dense-in-itself for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is perfect holds
( b1 is closed & b1 is dense-in-itself ) by Def10;
cluster closed dense-in-itself  ->  perfect for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is closed & b1 is dense-in-itself holds
b1 is perfect by Def10;
end;

theorem Th40: :: TOPGEN_1:40
for T being TopSpace holds Der ({} T) = {} T
proof
let T be TopSpace; ::_thesis: Der ({} T) = {} T
 Cl ({} T) is empty ;
then  {} = ({} T) \/ (Der ({} T)) by Th29
.= Der ({} T) ;
hence  Der ({} T) = {} T ; ::_thesis: verum
end;

Lm1:  for T being TopSpace
for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A
let A be Subset of T; ::_thesis: ( A is closed & A is dense-in-itself implies Der A = A )
assume A1: ( A is closed & A is dense-in-itself ) ; ::_thesis: Der A = A
then A = Cl A by PRE_TOPC:22
.= (Der A) \/ A by Th29 ;
hence  Der A c= A by XBOOLE_1:7; :: according to XBOOLE_0:def_10 ::_thesis: A c= Der A
thus  A c= Der A by A1, Def7; ::_thesis: verum
end;

theorem Th41: :: TOPGEN_1:41
for T being TopSpace
for A being Subset of T holds
( A is perfect iff Der A = A )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is perfect iff Der A = A )
let A be Subset of T; ::_thesis: ( A is perfect iff Der A = A )
thus  ( A is perfect implies Der A = A ) by Lm1; ::_thesis: ( Der A = A implies A is perfect )
assume A1: Der A = A ; ::_thesis: A is perfect
A2: Cl A = (Der A) \/ A by Th29
.= A by A1 ;
 A is dense-in-itself by A1, Def7;
hence  A is perfect by A2; ::_thesis: verum
end;

theorem Th42: :: TOPGEN_1:42
for T being TopSpace holds {} T is perfect
proof
let T be TopSpace; ::_thesis: {} T is perfect
 Der ({} T) = {} T by Th40;
hence  {} T is perfect by Th41; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster empty  ->  perfect for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is perfect
proof
let A be Subset of T; ::_thesis: ( A is empty implies A is perfect )
assume  A is empty ; ::_thesis: A is perfect
then  A = {} T ;
hence  A is perfect by Th42; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster perfect for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st b1 is perfect
proof
take  {} T ; ::_thesis: {} T is perfect
thus  {} T is perfect ; ::_thesis: verum
end;
end;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA is scattered  means :Def11: :: TOPGEN_1:def 11
 for B being Subset of T holds
( B is empty or not B c= A or not B is dense-in-itself );
end;

:: deftheorem Def11 defines scattered TOPGEN_1:def_11_:_
 for T being TopSpace
for A being Subset of T holds
( A is scattered iff for B being Subset of T holds
( B is empty or not B c= A or not B is dense-in-itself ) );

registration
let T be non empty TopSpace;
cluster non empty scattered  ->  non dense-in-itself for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st not b1 is empty & b1 is scattered holds
not b1 is dense-in-itself by Def11;
cluster non empty dense-in-itself  ->  non scattered for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is dense-in-itself & not b1 is empty holds
not b1 is scattered ;
end;

theorem Th43: :: TOPGEN_1:43
for T being TopSpace holds {} T is scattered
proof
let T be TopSpace; ::_thesis: {} T is scattered
 {} T is scattered
proof
assume  not {} T is scattered ; ::_thesis: contradiction
then  ex B being Subset of T st
( not B is empty & B c= {} T & B is dense-in-itself ) by Def11;
hence  contradiction ; ::_thesis: verum
end;
hence  {} T is scattered ; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster empty  ->  scattered for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is scattered
proof
let A be Subset of T; ::_thesis: ( A is empty implies A is scattered )
assume  A is empty ; ::_thesis: A is scattered
then  A = {} T ;
hence  A is scattered by Th43; ::_thesis: verum
end;
end;

theorem :: TOPGEN_1:44
for T being non empty TopSpace st T is T_1 holds
ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered )
proof
let T be non empty TopSpace; ::_thesis: ( T is T_1 implies ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered ) )
defpred S1[ Subset of T] means $1 is dense-in-itself ;
consider CC being Subset-Family of T such that
A1: for A being Subset of T holds
( A in CC iff S1[A] ) from SUBSET_1:sch_3();
set C = union CC;
A2: ( [#] T = (union CC) \/ ((union CC) `) & union CC misses (union CC) ` ) by PRE_TOPC:2, XBOOLE_1:79;
A3: CC is dense-in-itself by A1, Def9;
assume  T is T_1 ; ::_thesis: ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered )
then  Cl (union CC) is dense-in-itself by A3, Th36, Th38;
then  Cl (union CC) in CC by A1;
then A4: Cl (union CC) c= union CC by ZFMISC_1:74;
 union CC c= Cl (union CC) by PRE_TOPC:18;
then A5: Cl (union CC) = union CC by A4, XBOOLE_0:def_10;
 for B being Subset of T holds
( B is empty or not B c= (union CC) ` or not B is dense-in-itself )
proof
given B being Subset of T such that A6: not B is empty and
A7: ( B c= (union CC) ` & B is dense-in-itself ) ; ::_thesis: contradiction
 ( B misses union CC & B in CC ) by A1, A7, SUBSET_1:23;
hence  contradiction by A6, XBOOLE_1:69, ZFMISC_1:74; ::_thesis: verum
end;
then A8: (union CC) ` is scattered by Def11;
 union CC is dense-in-itself by A3, Th38;
hence  ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered ) by A5, A8, A2; ::_thesis: verum
end;

registration
let T be discrete TopSpace;
let A be Subset of T;
cluster Fr A ->  empty ;
coherence
 Fr A is empty
proof
 ( A is open & A is closed ) by TDLAT_3:15, TDLAT_3:16;
hence  Fr A is empty ; ::_thesis: verum
end;
end;

registration
let T be discrete TopSpace;
cluster  ->  open closed for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T holds
( b1 is closed & b1 is open ) by TDLAT_3:15, TDLAT_3:16;
end;

theorem Th45: :: TOPGEN_1:45
for T being discrete TopSpace
for A being Subset of T holds Der A = {}
proof
let T be discrete TopSpace; ::_thesis: for A being Subset of T holds Der A = {}
let A be Subset of T; ::_thesis: Der A = {}
percases ( not T is empty or T is empty ) ;
supposeA1: not T is empty ; ::_thesis: Der A = {}
assume  Der A <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in Der A by XBOOLE_0:def_1;
 x is_an_accumulation_point_of A by A1, A2, Th16;
then  x in Cl (A \ {x}) by Def2;
then  x in A \ {x} by PRE_TOPC:22;
hence  contradiction by ZFMISC_1:56; ::_thesis: verum
end;
suppose T is empty ; ::_thesis: Der A = {}
then  the carrier of T is empty ;
hence  Der A = {} ; ::_thesis: verum
end;
end;
end;

registration
let T be non empty discrete TopSpace;
let A be Subset of T;
cluster Der A ->  empty ;
coherence
 Der A is empty by Th45;
end;

begin

definition
let T be TopSpace;
func density T ->  cardinal number  means :Def12: :: TOPGEN_1:def 12
( ex A being Subset of T st
( A is dense & it = card A ) & ( for B being Subset of T st B is dense holds
it c= card B ) );
existence
 ex b1 being cardinal number st
( ex A being Subset of T st
( A is dense & b1 = card A ) & ( for B being Subset of T st B is dense holds
b1 c= card B ) )
proof
set B0 = [#] T;
defpred S1[ ordinal number ] means  ex A being Subset of T st
( A is dense & $1 = card A );
 card ([#] T) is ordinal ;
then A1: ex A being ordinal number st S1[A] ;
consider A being ordinal number  such that
A2: S1[A] and
A3: for B being ordinal number st S1[B] holds
A c= B from ORDINAL1:sch_1(A1);
consider B1 being Subset of T such that
A4: ( B1 is dense & A = card B1 ) by A2;
take  card B1 ; ::_thesis: ( ex A being Subset of T st
( A is dense & card B1 = card A ) & ( for B being Subset of T st B is dense holds
card B1 c= card B ) )
thus  ( ex A being Subset of T st
( A is dense & card B1 = card A ) & ( for B being Subset of T st B is dense holds
card B1 c= card B ) ) by A3, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being cardinal number st ex A being Subset of T st
( A is dense & b1 = card A ) & ( for B being Subset of T st B is dense holds
b1 c= card B ) & ex A being Subset of T st
( A is dense & b2 = card A ) & ( for B being Subset of T st B is dense holds
b2 c= card B ) holds
b1 = b2
proof
let M1, M2 be cardinal number ; ::_thesis: ( ex A being Subset of T st
( A is dense & M1 = card A ) & ( for B being Subset of T st B is dense holds
M1 c= card B ) & ex A being Subset of T st
( A is dense & M2 = card A ) & ( for B being Subset of T st B is dense holds
M2 c= card B ) implies M1 = M2 )
assume  ( ex B being Subset of T st
( B is dense & M1 = card B ) & ( for B being Subset of T st B is dense holds
M1 c= card B ) & ex B being Subset of T st
( B is dense & M2 = card B ) & ( for B being Subset of T st B is dense holds
M2 c= card B ) ) ; ::_thesis: M1 = M2
hence  ( M1 c= M2 & M2 c= M1 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem Def12 defines density TOPGEN_1:def_12_:_
 for T being TopSpace
for b2 being cardinal number holds
( b2 = density T iff ( ex A being Subset of T st
( A is dense & b2 = card A ) & ( for B being Subset of T st B is dense holds
b2 c= card B ) ) );

definition
let T be TopSpace;
attrT is separable  means :Def13: :: TOPGEN_1:def 13
 density T c= omega ;
end;

:: deftheorem Def13 defines separable TOPGEN_1:def_13_:_
 for T being TopSpace holds
( T is separable iff density T c= omega );

theorem Th46: :: TOPGEN_1:46
for T being countable TopSpace holds T is separable
proof
let T be countable TopSpace; ::_thesis: T is separable
 ( card ([#] T) c= omega & density T c= card ([#] T) ) by Def12, CARD_3:def_14;
then  density T c= omega by XBOOLE_1:1;
hence  T is separable by Def13; ::_thesis: verum
end;

registration
cluster TopSpace-like countable  ->  separable for TopStruct ;
coherence
 for b1 being TopSpace st b1 is countable holds
b1 is separable by Th46;
end;

begin

theorem :: TOPGEN_1:47
for A being Subset of R^1 st A = RAT holds
A ` = IRRAT by BORSUK_5:def_1, TOPMETR:17;

Lm2:  RAT = REAL \ IRRAT
proof
 REAL \ IRRAT = REAL /\ RAT by BORSUK_5:def_1, XBOOLE_1:48;
hence  RAT = REAL \ IRRAT by NUMBERS:12, XBOOLE_1:28; ::_thesis: verum
end;

theorem :: TOPGEN_1:48
for A being Subset of R^1 st A = IRRAT holds
A ` = RAT by Lm2, TOPMETR:17;

theorem :: TOPGEN_1:49
for A being Subset of R^1 st A = RAT holds
Int A = {}
proof
let A be Subset of R^1; ::_thesis: ( A = RAT implies Int A = {} )
assume  A = RAT ; ::_thesis: Int A = {}
then  Cl (A `) = [#] R^1 by BORSUK_5:28, BORSUK_5:def_1, TOPMETR:17;
then  (Cl (A `)) ` = {} R^1 by XBOOLE_1:37;
hence  Int A = {} by Th3; ::_thesis: verum
end;

theorem :: TOPGEN_1:50
for A being Subset of R^1 st A = IRRAT holds
Int A = {}
proof
let A be Subset of R^1; ::_thesis: ( A = IRRAT implies Int A = {} )
assume  A = IRRAT ; ::_thesis: Int A = {}
then  Cl (A `) = [#] R^1 by Lm2, BORSUK_5:15, TOPMETR:17;
then  (Cl (A `)) ` = {} R^1 by XBOOLE_1:37;
hence  Int A = {} by Th3; ::_thesis: verum
end;

reconsider B = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;

theorem Th51: :: TOPGEN_1:51
RAT is dense Subset of R^1
proof
 Cl B = the carrier of R^1 by BORSUK_5:15;
hence  RAT is dense Subset of R^1 by TOPS_3:def_2; ::_thesis: verum
end;

reconsider A = IRRAT as Subset of R^1 by TOPMETR:17;

theorem Th52: :: TOPGEN_1:52
IRRAT is dense Subset of R^1
proof
 Cl A = the carrier of R^1 by BORSUK_5:28;
hence  IRRAT is dense Subset of R^1 by TOPS_3:def_2; ::_thesis: verum
end;

theorem Th53: :: TOPGEN_1:53
RAT is boundary Subset of R^1
proof
 B ` is dense by Th52, BORSUK_5:def_1, TOPMETR:17;
hence  RAT is boundary Subset of R^1 by TOPS_1:def_4; ::_thesis: verum
end;

theorem Th54: :: TOPGEN_1:54
IRRAT is boundary Subset of R^1
proof
 A ` is dense by Lm2, Th51, TOPMETR:17;
hence  IRRAT is boundary Subset of R^1 by TOPS_1:def_4; ::_thesis: verum
end;

theorem Th55: :: TOPGEN_1:55
REAL is non boundary Subset of R^1
proof
reconsider A = [#] REAL as Subset of R^1 by TOPMETR:17;
 [#] R^1 = REAL by TOPMETR:17;
hence  REAL is non boundary Subset of R^1 ; ::_thesis: verum
end;

theorem :: TOPGEN_1:56
ex A, B being Subset of R^1 st
( A is boundary & B is boundary & not A \/ B is boundary )
proof
reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
reconsider A = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;
take  A ; ::_thesis: ex B being Subset of R^1 st
( A is boundary & B is boundary & not A \/ B is boundary )
take  B ; ::_thesis: ( A is boundary & B is boundary & not A \/ B is boundary )
A \/ B = RAT \/ REAL by BORSUK_5:def_1, XBOOLE_1:39
.= REAL by NUMBERS:12, XBOOLE_1:12 ;
hence  ( A is boundary & B is boundary & not A \/ B is boundary ) by Th53, Th54, Th55; ::_thesis: verum
end;