:: TOPGEN_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let T be 1-sorted ;
func TotFam T -> Subset-Family of T equals :: TOPGEN_4:def 1
bool the carrier of T;
coherence
bool the carrier of T is Subset-Family of T
;
end;

:: deftheorem defines TotFam TOPGEN_4:def 1 :
for T being 1-sorted holds TotFam T = bool the carrier of T;

theorem Th1: :: TOPGEN_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )
proof end;

registration
cluster RAT -> countable ;
coherence
RAT is countable
by CARD_4:def 1, TOPGEN_3:17;
end;

Lm1: for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
proof end;

scheme :: TOPGEN_4:sch 1
FraenCoun11{ P1[ set ] } :
{ {n} where n is Element of RAT : P1[n] } is countable
proof end;

theorem :: TOPGEN_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds Der A = { x where x is Point of T : x in Cl (A \ {x}) }
proof end;

registration
cluster finite -> second-countable TopStruct ;
coherence
for b1 being TopStruct st b1 is finite holds
b1 is second-countable
proof end;
end;

registration
cluster REAL -> non countable ;
coherence
not REAL is countable
proof end;
end;

registration
cluster non countable -> non finite set ;
coherence
for b1 being set st not b1 is countable holds
not b1 is finite
by CARD_4:43;
cluster non finite -> non trivial set ;
coherence
for b1 being set st not b1 is finite holds
not b1 is trivial
proof end;
cluster non empty non countable set ;
existence
ex b1 being set st
( not b1 is countable & not b1 is empty )
proof end;
end;

theorem :: TOPGEN_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff Der A c= A )
proof end;

theorem Th4: :: TOPGEN_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopStruct
for B being Basis of T
for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
proof end;

theorem Th5: :: TOPGEN_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds density T <=` weight T
proof end;

theorem :: TOPGEN_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( T is separable iff ex A being Subset of T st
( A is dense & A is countable ) )
proof end;

theorem Th7: :: TOPGEN_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is second-countable holds
T is separable
proof end;

registration
cluster non empty second-countable -> non empty separable TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is second-countable holds
b1 is separable
by Th7;
end;

theorem :: TOPGEN_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st A,B are_separated holds
Fr (A \/ B) = (Fr A) \/ (Fr B)
proof end;

theorem :: TOPGEN_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F being Subset-Family of T st F is locally_finite holds
Fr (union F) c= union (Fr F)
proof end;

theorem Th10: :: TOPGEN_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty discrete TopSpace holds
( T is separable iff Card ([#] T) <=` alef 0 )
proof end;

theorem :: TOPGEN_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty discrete TopSpace holds
( T is separable iff T is countable )
proof end;

definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attr F is all-open-containing means :Def2: :: TOPGEN_4:def 2
for A being Subset of T st A is open holds
A in F;
end;

:: deftheorem Def2 defines all-open-containing TOPGEN_4:def 2 :
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-open-containing iff for A being Subset of T st A is open holds
A in F );

definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attr F is all-closed-containing means :Def3: :: TOPGEN_4:def 3
for A being Subset of T st A is closed holds
A in F;
end;

:: deftheorem Def3 defines all-closed-containing TOPGEN_4:def 3 :
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing iff for A being Subset of T st A is closed holds
A in F );

definition
let T be set ;
let F be Subset-Family of T;
attr F is closed_for_countable_unions means :Def4: :: TOPGEN_4:def 4
for G being countable Subset-Family of T st G c= F holds
union G in F;
end;

:: deftheorem Def4 defines closed_for_countable_unions TOPGEN_4:def 4 :
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_unions iff for G being countable Subset-Family of T st G c= F holds
union G in F );

Lm2: for T being set
for F being Subset-Family of T st F is sigma_Field_Subset of T holds
F is closed_for_countable_unions
proof end;

registration
let T be set ;
cluster -> closed_for_countable_unions Element of K10(K10(T));
coherence
for b1 being sigma_Field_Subset of T holds b1 is closed_for_countable_unions
by Lm2;
end;

theorem Th12: :: TOPGEN_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F being Subset-Family of T st F is closed_for_countable_unions holds
{} in F
proof end;

registration
let T be set ;
cluster closed_for_countable_unions -> non empty Element of K10(K10(T));
coherence
for b1 being Subset-Family of T st b1 is closed_for_countable_unions holds
not b1 is empty
by Th12;
end;

theorem Th13: :: TOPGEN_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F being Subset-Family of T holds
( F is sigma_Field_Subset of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
proof end;

definition
let T be set ;
let F be Subset-Family of T;
attr F is closed_for_countable_meets means :Def5: :: TOPGEN_4:def 5
for G being countable Subset-Family of T st G c= F holds
meet G in F;
end;

:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def 5 :
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets iff for G being countable Subset-Family of T st G c= F holds
meet G in F );

theorem Th14: :: TOPGEN_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
proof end;

theorem :: TOPGEN_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
proof end;

theorem Th16: :: TOPGEN_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F, G being Subset-Family of T st F c= G & G is compl-closed holds
COMPLEMENT F c= G
proof end;

theorem Th17: :: TOPGEN_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )
proof end;

registration
let T be non empty TopSpace;
cluster compl-closed all-open-containing closed_for_countable_unions -> all-closed-containing closed_for_countable_meets Element of K10(K10(the carrier of T));
coherence
for b1 being Subset-Family of T st b1 is all-open-containing & b1 is compl-closed & b1 is closed_for_countable_unions holds
( b1 is all-closed-containing & b1 is closed_for_countable_meets )
by Th17, Th14;
cluster compl-closed all-closed-containing closed_for_countable_meets -> non empty all-open-containing closed_for_countable_unions Element of K10(K10(the carrier of T));
coherence
for b1 being Subset-Family of T st b1 is all-closed-containing & b1 is compl-closed & b1 is closed_for_countable_meets holds
( b1 is all-open-containing & b1 is closed_for_countable_unions )
by Th17, Th14;
end;

registration
let T be set ;
let F be countable Subset-Family of T;
cluster COMPLEMENT F -> countable ;
coherence
COMPLEMENT F is countable
by Th1;
end;

registration
let T be non empty TopSpace;
cluster empty -> open closed Element of K10(K10(the carrier of T));
coherence
for b1 being Subset-Family of T st b1 is empty holds
( b1 is open & b1 is closed )
proof end;
end;

registration
let T be non empty TopSpace;
cluster open closed countable Element of K10(K10(the carrier of T));
existence
ex b1 being Subset-Family of T st
( b1 is countable & b1 is open & b1 is closed )
proof end;
end;

theorem Th18: :: TOPGEN_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set holds {} is empty Subset-Family of T
proof end;

registration
cluster empty -> countable set ;
coherence
for b1 being set st b1 is empty holds
b1 is countable
proof end;
end;

theorem Th19: :: TOPGEN_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
proof end;

theorem Th20: :: TOPGEN_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
proof end;

definition
let T be set ;
let F, G be Subset-Family of T;
:: original: INTERSECTION
redefine func INTERSECTION F,G -> Subset-Family of T;
coherence
INTERSECTION F,G is Subset-Family of T
proof end;
:: original: UNION
redefine func UNION F,G -> Subset-Family of T;
coherence
UNION F,G is Subset-Family of T
proof end;
end;

theorem Th21: :: TOPGEN_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed & G is closed holds
INTERSECTION F,G is closed
proof end;

theorem Th22: :: TOPGEN_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed & G is closed holds
UNION F,G is closed
proof end;

theorem Th23: :: TOPGEN_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F, G being Subset-Family of T st F is open & G is open holds
INTERSECTION F,G is open
proof end;

theorem Th24: :: TOPGEN_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F, G being Subset-Family of T st F is open & G is open holds
UNION F,G is open
proof end;

theorem Th25: :: TOPGEN_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F, G being Subset-Family of T holds Card (INTERSECTION F,G) <=` Card [:F,G:]
proof end;

theorem Th26: :: TOPGEN_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for F, G being Subset-Family of T holds Card (UNION F,G) <=` Card [:F,G:]
proof end;

theorem Th27: :: TOPGEN_4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set holds union (UNION F,G) c= (union F) \/ (union G)
proof end;

theorem Th28: :: TOPGEN_4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set st F <> {} & G <> {} holds
(union F) \/ (union G) = union (UNION F,G)
proof end;

theorem Th29: :: TOPGEN_4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being set holds UNION {} ,F = {}
proof end;

theorem :: TOPGEN_4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set holds
( not UNION F,G = {} or F = {} or G = {} )
proof end;

theorem :: TOPGEN_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set holds
( not INTERSECTION F,G = {} or F = {} or G = {} )
proof end;

theorem Th32: :: TOPGEN_4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set holds meet (UNION F,G) c= (meet F) \/ (meet G)
proof end;

theorem :: TOPGEN_4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set st F <> {} & G <> {} holds
meet (UNION F,G) = (meet F) \/ (meet G)
proof end;

theorem Th34: :: TOPGEN_4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being set st F <> {} & G <> {} holds
(meet F) /\ (meet G) = meet (INTERSECTION F,G)
proof end;

definition
let T be non empty TopSpace;
let A be Subset of T;
attr A is F_sigma means :Def6: :: TOPGEN_4:def 6
ex F being closed countable Subset-Family of T st A = union F;
end;

:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :
for T being non empty TopSpace
for A being Subset of T holds
( A is F_sigma iff ex F being closed countable Subset-Family of T st A = union F );

definition
let T be non empty TopSpace;
let A be Subset of T;
attr A is G_delta means :Def7: :: TOPGEN_4:def 7
ex F being open countable Subset-Family of T st A = meet F;
end;

:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :
for T being non empty TopSpace
for A being Subset of T holds
( A is G_delta iff ex F being open countable Subset-Family of T st A = meet F );

theorem Th35: :: TOPGEN_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds {} T is F_sigma
proof end;

theorem Th36: :: TOPGEN_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds {} T is G_delta
proof end;

registration
let T be non empty TopSpace;
cluster {} T -> countable F_sigma G_delta ;
coherence
( {} T is F_sigma & {} T is G_delta )
by Th36, Th35;
end;

theorem Th37: :: TOPGEN_4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds [#] T is F_sigma
proof end;

theorem Th38: :: TOPGEN_4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds [#] T is G_delta
proof end;

registration
let T be non empty TopSpace;
cluster [#] T -> F_sigma G_delta ;
coherence
( [#] T is F_sigma & [#] T is G_delta )
by Th37, Th38;
end;

theorem :: TOPGEN_4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st A is F_sigma holds
A ` is G_delta
proof end;

theorem :: TOPGEN_4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st A is G_delta holds
A ` is F_sigma
proof end;

theorem :: TOPGEN_4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A /\ B is F_sigma
proof end;

theorem :: TOPGEN_4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A \/ B is F_sigma
proof end;

theorem :: TOPGEN_4:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st A is G_delta & B is G_delta holds
A \/ B is G_delta
proof end;

theorem :: TOPGEN_4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st A is G_delta & B is G_delta holds
A /\ B is G_delta
proof end;

theorem :: TOPGEN_4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st A is closed holds
A is F_sigma
proof end;

theorem :: TOPGEN_4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st A is open holds
A is G_delta
proof end;

theorem :: TOPGEN_4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Subset of R^1 st A = RAT holds
A is F_sigma
proof end;

definition
let T be TopSpace;
attr T is T_1/2 means :Def8: :: TOPGEN_4:def 8
for A being Subset of T holds Der A is closed;
end;

:: deftheorem Def8 defines T_1/2 TOPGEN_4:def 8 :
for T being TopSpace holds
( T is T_1/2 iff for A being Subset of T holds Der A is closed );

theorem Th48: :: TOPGEN_4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace st T is being_T1 holds
T is T_1/2
proof end;

theorem Th49: :: TOPGEN_4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is T_1/2 holds
T is T_0
proof end;

theorem :: TOPGEN_4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for p being Point of T holds
( p is_isolated_in [#] T or p is_an_accumulation_point_of [#] T )
proof end;

registration
cluster T_1/2 -> T_0 TopStruct ;
coherence
for b1 being TopSpace st b1 is T_1/2 holds
b1 is T_0
proof end;
cluster being_T1 -> T_1/2 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T1 holds
b1 is T_1/2
by Th48;
end;

definition
let T be non empty TopSpace;
let A be Subset of T;
let x be Point of T;
pred x is_a_condensation_point_of A means :Def9: :: TOPGEN_4:def 9
for N being a_neighborhood of x holds not N /\ A is countable;
end;

:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def 9 :
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x is_a_condensation_point_of A iff for N being a_neighborhood of x holds not N /\ A is countable );

theorem Th51: :: TOPGEN_4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T st x is_a_condensation_point_of A & A c= B holds
x is_a_condensation_point_of B
proof end;

definition
let T be non empty TopSpace;
let A be Subset of T;
func A ^0 -> Subset of T means :Def10: :: TOPGEN_4:def 10
for x being Point of T holds
( x in it iff x is_a_condensation_point_of A );
existence
ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A )
proof end;
uniqueness
for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A ) ) & ( for x being Point of T holds
( x in b2 iff x is_a_condensation_point_of A ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines ^0 TOPGEN_4:def 10 :
for T being non empty TopSpace
for A, b3 being Subset of T holds
( b3 = A ^0 iff for x being Point of T holds
( x in b3 iff x is_a_condensation_point_of A ) );

theorem Th52: :: TOPGEN_4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T
for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
proof end;

theorem :: TOPGEN_4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds A ^0 c= Der A
proof end;

theorem :: TOPGEN_4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds A ^0 = Cl (A ^0 )
proof end;

theorem Th55: :: TOPGEN_4:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
A ^0 c= B ^0
proof end;

theorem Th56: :: TOPGEN_4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
proof end;

theorem :: TOPGEN_4:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T holds (A \/ B) ^0 = (A ^0 ) \/ (B ^0 )
proof end;

theorem Th58: :: TOPGEN_4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st A is countable holds
for x being Point of T holds not x is_a_condensation_point_of A
proof end;

theorem Th59: :: TOPGEN_4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st A is countable holds
A ^0 = {}
proof end;

registration
let T be non empty TopSpace;
let A be countable Subset of T;
cluster A ^0 -> empty countable ;
coherence
A ^0 is empty
by Th59;
end;

theorem :: TOPGEN_4:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is second-countable holds
ex B being Basis of T st B is countable
proof end;

registration
cluster non empty second-countable separable TopStruct ;
existence
ex b1 being TopSpace st
( b1 is second-countable & not b1 is empty )
proof end;
end;

registration
let T be non empty TopSpace;
cluster TotFam T -> non empty compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets ;
coherence
( not TotFam T is empty & TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
proof end;
end;

theorem Th61: :: TOPGEN_4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being set
for A being SetSequence of T holds rng A is non empty countable Subset-Family of T
proof end;

theorem Th62: :: TOPGEN_4:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, F being set holds
( F is SigmaField of T iff F is sigma_Field_Subset of T )
proof end;

theorem Th63: :: TOPGEN_4:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-open-containing & F c= G holds
G is all-open-containing
proof end;

theorem :: TOPGEN_4:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds
G is all-closed-containing
proof end;

definition
let T be 1-sorted ;
mode SigmaField of T is SigmaField of the carrier of T;
mode sigma_Field_Subset of T is sigma_Field_Subset of the carrier of T;
end;

registration
let T be non empty TopSpace;
cluster non empty compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets Element of K10(K10(the carrier of T));
existence
ex b1 being Subset-Family of T st
( b1 is compl-closed & b1 is closed_for_countable_unions & b1 is closed_for_countable_meets & b1 is all-closed-containing & b1 is all-open-containing )
proof end;
end;

theorem Th65: :: TOPGEN_4:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
proof end;

registration
let T be non empty TopSpace;
cluster sigma (TotFam T) -> compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets ;
coherence
( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
by Th65;
end;

registration
let T be non empty 1-sorted ;
cluster non empty compl-closed sigma_Field_Subset-like closed_for_countable_unions Element of K10(K10(the carrier of T));
existence
ex b1 being Subset-Family of T st
( b1 is sigma_Field_Subset-like & b1 is compl-closed & b1 is closed_for_countable_unions & not b1 is empty )
proof end;
end;

registration
let T be non empty TopSpace;
cluster -> non empty closed_for_countable_unions SigmaField of the carrier of T;
coherence
for b1 being SigmaField of T holds b1 is closed_for_countable_unions
by Th62;
end;

theorem Th66: :: TOPGEN_4:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F being Subset-Family of T st F is compl-closed & F is closed_for_countable_unions holds
F is SigmaField of T
proof end;

registration
let T be non empty TopSpace;
cluster all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets SigmaField of the carrier of T;
existence
ex b1 being SigmaField of T st b1 is all-open-containing
proof end;
end;

registration
let T be non empty TopSpace;
cluster Topology_of T -> open all-open-containing ;
coherence
( Topology_of T is open & Topology_of T is all-open-containing )
proof end;
end;

theorem Th67: :: TOPGEN_4:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
proof end;

definition
let T be non empty TopSpace;
func BorelSets T -> compl-closed all-open-containing closed_for_countable_unions Subset-Family of T means :Def11: :: TOPGEN_4:def 11
for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds it c= G;
existence
ex b1 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b1 c= G
proof end;
uniqueness
for b1, b2 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :
for T being non empty TopSpace
for b2 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
( b2 = BorelSets T iff for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G );

theorem Th68: :: TOPGEN_4:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F being closed Subset-Family of T holds F c= BorelSets T
proof end;

theorem Th69: :: TOPGEN_4:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for F being open Subset-Family of T holds F c= BorelSets T
proof end;

theorem :: TOPGEN_4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds BorelSets T = sigma (Topology_of T)
proof end;

definition
let T be non empty TopSpace;
let A be Subset of T;
attr A is Borel means :Def12: :: TOPGEN_4:def 12
A in BorelSets T;
end;

:: deftheorem Def12 defines Borel TOPGEN_4:def 12 :
for T being non empty TopSpace
for A being Subset of T holds
( A is Borel iff A in BorelSets T );

registration
let T be non empty TopSpace;
cluster F_sigma -> Borel Element of K10(the carrier of T);
coherence
for b1 being Subset of T st b1 is F_sigma holds
b1 is Borel
proof end;
end;

registration
let T be non empty TopSpace;
cluster G_delta -> Borel Element of K10(the carrier of T);
coherence
for b1 being Subset of T st b1 is G_delta holds
b1 is Borel
proof end;
end;