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

definition
let X be set ;
let B be Subset-Family of X;
attr B is point-filtered means :Def1: :: TOPGEN_3:def 1
for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds
ex U being Subset of X st
( U in B & x in U & U c= U1 /\ U2 );
end;

:: deftheorem Def1 defines point-filtered TOPGEN_3:def 1 :
for X being set
for B being Subset-Family of X holds
( B is point-filtered iff for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds
ex U being Subset of X st
( U in B & x in U & U c= U1 /\ U2 ) );

theorem Th1: :: TOPGEN_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for B being Subset-Family of X holds
( B is covering iff for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U ) )
proof end;

theorem Th2: :: TOPGEN_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for B being Subset-Family of X st B is point-filtered & B is covering holds
for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds
( T is TopSpace & B is Basis of T )
proof end;

theorem :: TOPGEN_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for B being V7 ManySortedSet of X st rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds
x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 ) ) holds
ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T' being non empty TopSpace st T' = T holds
B is Neighborhood_System of T' ) ) ) )
proof end;

theorem Th4: :: TOPGEN_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for F being Subset-Family of X st {} in F & X in F & ( for A, B being set st A in F & B in F holds
A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds
Intersect G in F ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )
proof end;

scheme :: TOPGEN_3:sch 1
TopDefByClosedPred{ F1() -> set , P1[ set ] } :
ex T being strict TopSpace st
( the carrier of T = F1() & ( for A being Subset of T holds
( A is closed iff P1[A] ) ) )
provided
A1: ( P1[ {} ] & P1[F1()] ) and
A2: for A, B being set st P1[A] & P1[B] holds
P1[A \/ B] and
A3: for G being Subset-Family of F1() st ( for A being set st A in G holds
P1[A] ) holds
P1[ Intersect G]
proof end;

Lm1: for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
proof end;

theorem :: TOPGEN_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #)
proof end;

Lm2: for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
proof end;

theorem Th6: :: TOPGEN_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #)
proof end;

definition
let X, Y be set ;
let r be Subset of [:X,(bool Y):];
:: original: rng
redefine func rng r -> Subset-Family of Y;
coherence
rng r is Subset-Family of Y
proof end;
end;

theorem Th7: :: TOPGEN_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for c being Function of bool X, bool X st c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds
( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )
proof end;

scheme :: TOPGEN_3:sch 2
TopDefByClosureOp{ F1() -> set , F2( set ) -> set } :
ex T being strict TopSpace st
( the carrier of T = F1() & ( for A being Subset of T holds Cl A = F2(A) ) )
provided
A1: F2({} ) = {} and
A2: for A being Subset of F1() holds
( A c= F2(A) & F2(A) c= F1() ) and
A3: for A, B being Subset of F1() holds F2((A \/ B)) = F2(A) \/ F2(B) and
A4: for A being Subset of F1() holds F2(F2(A)) = F2(A)
proof end;

theorem Th8: :: TOPGEN_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Cl A1 = Cl A2 ) holds
the topology of T1 = the topology of T2
proof end;

theorem Th9: :: TOPGEN_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for i being Function of bool X, bool X st i . X = X & ( for A being Subset of X holds i . A c= A ) & ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) & ( for A being Subset of X holds i . (i . A) = i . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = rng i holds
( T is TopSpace & ( for A being Subset of T holds Int A = i . A ) )
proof end;

scheme :: TOPGEN_3:sch 3
TopDefByInteriorOp{ F1() -> set , F2( set ) -> set } :
ex T being strict TopSpace st
( the carrier of T = F1() & ( for A being Subset of T holds Int A = F2(A) ) )
provided
A1: F2(F1()) = F1() and
A2: for A being Subset of F1() holds F2(A) c= A and
A3: for A, B being Subset of F1() holds F2((A /\ B)) = F2(A) /\ F2(B) and
A4: for A being Subset of F1() holds F2(F2(A)) = F2(A)
proof end;

theorem Th10: :: TOPGEN_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Int A1 = Int A2 ) holds
the topology of T1 = the topology of T2
proof end;

definition
func Sorgenfrey-line -> non empty strict TopSpace means :Def2: :: TOPGEN_3:def 2
( the carrier of it = REAL & ex B being Subset-Family of REAL st
( the topology of it = UniCl B & B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ) );
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = REAL & ex B being Subset-Family of REAL st
( the topology of b1 = UniCl B & B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ) & the carrier of b2 = REAL & ex B being Subset-Family of REAL st
( the topology of b2 = UniCl B & B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ) holds
b1 = b2
;
existence
ex b1 being non empty strict TopSpace st
( the carrier of b1 = REAL & ex B being Subset-Family of REAL st
( the topology of b1 = UniCl B & B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ) )
proof end;
end;

:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def 2 :
for b1 being non empty strict TopSpace holds
( b1 = Sorgenfrey-line iff ( the carrier of b1 = REAL & ex B being Subset-Family of REAL st
( the topology of b1 = UniCl B & B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ) ) );

Lm3: the carrier of Sorgenfrey-line = REAL
by Def2;

consider BB being Subset-Family of REAL such that
Lm4: the topology of Sorgenfrey-line = UniCl BB and
Lm5: BB = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } by Def2;

BB c= the topology of Sorgenfrey-line
by Lm4, CANTOR_1:1;

then Lm6: BB is Basis of Sorgenfrey-line
by Lm3, Lm4, CANTOR_1:def 2;

theorem Th11: :: TOPGEN_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds [.x,y.[ is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds ].x,y.[ is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds left_open_halfline x is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds right_open_halfline x is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds right_closed_halfline x is open Subset of Sorgenfrey-line
proof end;

theorem Th16: :: TOPGEN_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Card INT = alef 0
proof end;

theorem Th17: :: TOPGEN_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Card RAT = alef 0
proof end;

theorem Th18: :: TOPGEN_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set st A is mutually-disjoint & ( for a being set st a in A holds
ex x, y being real number st
( x < y & ].x,y.[ c= a ) ) holds
A is countable
proof end;

definition
let X be set ;
let x be real number ;
pred x is_local_minimum_of X means :Def3: :: TOPGEN_3:def 3
( x in X & ex y being real number st
( y < x & ].y,x.[ misses X ) );
end;

:: deftheorem Def3 defines is_local_minimum_of TOPGEN_3:def 3 :
for X being set
for x being real number holds
( x is_local_minimum_of X iff ( x in X & ex y being real number st
( y < x & ].y,x.[ misses X ) ) );

theorem Th19: :: TOPGEN_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for U being Subset of REAL holds { x where x is Element of REAL : x is_local_minimum_of U } is countable
proof end;

registration
cluster INT -> infinite ;
coherence
not INT is finite
by NUMBERS:17, FINSET_1:13;
cluster RAT -> infinite ;
coherence
not RAT is finite
by NUMBERS:18, FINSET_1:13;
cluster REAL -> infinite ;
coherence
not REAL is finite
proof end;
let X be infinite set ;
cluster bool X -> infinite ;
coherence
not bool X is finite
by FINSET_1:24;
end;

registration
let M be Aleph;
cluster exp 2,M -> infinite ;
coherence
not exp 2,M is finite
proof end;
end;

definition
func continuum -> infinite cardinal number equals :: TOPGEN_3:def 4
Card REAL ;
coherence
Card REAL is infinite cardinal number
;
end;

:: deftheorem defines continuum TOPGEN_3:def 4 :
continuum = Card REAL ;

theorem Th20: :: TOPGEN_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } = continuum
proof end;

registration
let X be infinite set ;
cluster infinite Element of bool X;
existence
not for b1 being Subset of X holds b1 is finite
proof end;
end;

definition
let X be set ;
let r be real number ;
func X -powers r -> Function of NAT , REAL means :Def5: :: TOPGEN_3:def 5
for i being natural number holds
( ( i in X & it . i = r |^ i ) or ( not i in X & it . i = 0 ) );
existence
ex b1 being Function of NAT , REAL st
for i being natural number holds
( ( i in X & b1 . i = r |^ i ) or ( not i in X & b1 . i = 0 ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , REAL st ( for i being natural number holds
( ( i in X & b1 . i = r |^ i ) or ( not i in X & b1 . i = 0 ) ) ) & ( for i being natural number holds
( ( i in X & b2 . i = r |^ i ) or ( not i in X & b2 . i = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :
for X being set
for r being real number
for b3 being Function of NAT , REAL holds
( b3 = X -powers r iff for i being natural number holds
( ( i in X & b3 . i = r |^ i ) or ( not i in X & b3 . i = 0 ) ) );

theorem Th21: :: TOPGEN_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for r being real number st 0 < r & r < 1 holds
X -powers r is summable
proof end;

theorem Th22: :: TOPGEN_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq ) ^\ n) = (r |^ n) / (1 - r)
proof end;

theorem Th23: :: TOPGEN_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Element of NAT holds Sum (((1 / 2) GeoSeq ) ^\ (n + 1)) = (1 / 2) |^ n
proof end;

theorem :: TOPGEN_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq )
proof end;

theorem Th25: :: TOPGEN_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n
proof end;

theorem Th26: :: TOPGEN_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite Subset of NAT
for i being natural number holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
proof end;

theorem Th27: :: TOPGEN_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being infinite Subset of NAT st Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) holds
X = Y
proof end;

theorem Th28: :: TOPGEN_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is countable holds
Fin X is countable
proof end;

theorem Th29: :: TOPGEN_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
continuum = exp 2,(alef 0)
proof end;

theorem Th30: :: TOPGEN_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
alef 0 <` continuum
proof end;

theorem Th31: :: TOPGEN_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Subset-Family of REAL st Card A <` continuum holds
Card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U )
}
<` continuum
proof end;

theorem Th32: :: TOPGEN_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset-Family of REAL st Card X <` continuum holds
ex x being real number ex q being rational number st
( x < q & not [.x,q.[ in UniCl X )
proof end;

theorem :: TOPGEN_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
weight Sorgenfrey-line = continuum
proof end;

definition
let X be set ;
func ClFinTop X -> strict TopSpace means :Def6: :: TOPGEN_3:def 6
( the carrier of it = X & ( for F being Subset of it holds
( F is closed iff ( F is finite or F = X ) ) ) );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = X & ( for F being Subset of b1 holds
( F is closed iff ( F is finite or F = X ) ) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for F being Subset of b1 holds
( F is closed iff ( F is finite or F = X ) ) ) & the carrier of b2 = X & ( for F being Subset of b2 holds
( F is closed iff ( F is finite or F = X ) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :
for X being set
for b2 being strict TopSpace holds
( b2 = ClFinTop X iff ( the carrier of b2 = X & ( for F being Subset of b2 holds
( F is closed iff ( F is finite or F = X ) ) ) ) );

theorem Th34: :: TOPGEN_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset of (ClFinTop X) holds
( A is open iff ( A = {} or A ` is finite ) )
proof end;

theorem Th35: :: TOPGEN_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for A being Subset of X st A is finite holds
not A ` is finite
proof end;

registration
let X be non empty set ;
cluster ClFinTop X -> non empty strict ;
coherence
not ClFinTop X is empty
proof end;
end;

theorem :: TOPGEN_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for U, V being non empty open Subset of (ClFinTop X) holds U meets V
proof end;

definition
let X, x0 be set ;
func x0 -PointClTop X -> strict TopSpace means :Def7: :: TOPGEN_3:def 7
( the carrier of it = X & ( for A being Subset of it holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = X & ( for A being Subset of b1 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for A being Subset of b1 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) & the carrier of b2 = X & ( for A being Subset of b2 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :
for X, x0 being set
for b3 being strict TopSpace holds
( b3 = x0 -PointClTop X iff ( the carrier of b3 = X & ( for A being Subset of b3 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) ) );

registration
let X be non empty set ;
let x0 be set ;
cluster x0 -PointClTop X -> non empty strict ;
coherence
not x0 -PointClTop X is empty
proof end;
end;

theorem Th37: :: TOPGEN_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}
proof end;

theorem Th38: :: TOPGEN_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds
( A is closed iff x0 in A )
proof end;

registration
let X be non empty set ;
let A be proper Subset of X;
cluster A ` -> non empty ;
coherence
not A ` is empty
proof end;
end;

theorem Th39: :: TOPGEN_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x0 being Element of X
for A being proper Subset of (x0 -PointClTop X) holds
( A is open iff not x0 in A )
proof end;

theorem :: TOPGEN_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0, x being set st x0 in X holds
( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 )
proof end;

theorem :: TOPGEN_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0, x being set st {x0} c< X holds
( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) )
proof end;

definition
let X, X0 be set ;
func X0 -DiscreteTop X -> strict TopSpace means :Def8: :: TOPGEN_3:def 8
( the carrier of it = X & ( for A being Subset of it holds Int A = IFEQ A,X,A,(A /\ X0) ) );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = X & ( for A being Subset of b1 holds Int A = IFEQ A,X,A,(A /\ X0) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for A being Subset of b1 holds Int A = IFEQ A,X,A,(A /\ X0) ) & the carrier of b2 = X & ( for A being Subset of b2 holds Int A = IFEQ A,X,A,(A /\ X0) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :
for X, X0 being set
for b3 being strict TopSpace holds
( b3 = X0 -DiscreteTop X iff ( the carrier of b3 = X & ( for A being Subset of b3 holds Int A = IFEQ A,X,A,(A /\ X0) ) ) );

registration
let X be non empty set ;
let X0 be set ;
cluster X0 -DiscreteTop X -> non empty strict ;
coherence
not X0 -DiscreteTop X is empty
proof end;
end;

theorem Th42: :: TOPGEN_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0
proof end;

theorem Th43: :: TOPGEN_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds
( A is open iff A c= X0 )
proof end;

Lm7: for X being set
for A being Subset of X st A is proper holds
not X is empty
proof end;

theorem Th44: :: TOPGEN_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)
proof end;

theorem :: TOPGEN_3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds ADTS X = {} -DiscreteTop X
proof end;

theorem :: TOPGEN_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds 1TopSp X = X -DiscreteTop X
proof end;