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

theorem Th1: :: TEX_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 non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
proof end;

Lm1: for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
proof end;

Lm2: for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
proof end;

theorem Th2: :: TEX_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 non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
proof end;

theorem :: TEX_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 non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is boundary iff B is dense ) by Th2;

theorem Th4: :: TEX_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 non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
proof end;

theorem :: TEX_3:5  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 TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is nowhere_dense iff B is everywhere_dense ) by Th4;

theorem Th6: :: TEX_3:6  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 TopSpace
for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
proof end;

theorem :: TEX_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 non empty non trivial TopSpace
for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
proof end;

theorem Th8: :: TEX_3:8  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 non trivial TopSpace
for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
proof end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is dense means :Def1: :: TEX_3:def 1
for A being Subset of X st A = the carrier of IT holds
A is dense;
end;

:: deftheorem Def1 defines dense TEX_3:def 1 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is dense iff for A being Subset of X st A = the carrier of IT holds
A is dense );

theorem Th9: :: TEX_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 non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
proof end;

registration
let X be non empty TopSpace;
cluster closed dense -> non proper SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is closed holds
not b1 is proper
proof end;
cluster proper dense -> non closed SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is closed
proof end;
cluster closed proper -> non dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper & b1 is closed holds
not b1 is dense
proof end;
end;

registration
let X be non empty TopSpace;
cluster non empty strict dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th10: :: TEX_3:10  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 TopSpace
for A0 being non empty Subset of X st A0 is dense holds
ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:11  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 TopSpace
for X0 being non empty dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
proof end;

theorem :: TEX_3:12  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 TopSpace
for X1 being dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
proof end;

theorem :: TEX_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 non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
proof end;

theorem :: TEX_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 non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
proof end;

theorem :: TEX_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1,the topology of Y1 #) holds
( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )
proof end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is everywhere_dense means :Def2: :: TEX_3:def 2
for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense;
end;

:: deftheorem Def2 defines everywhere_dense TEX_3:def 2 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense );

theorem Th16: :: TEX_3:16  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 TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
proof end;

registration
let X be non empty TopSpace;
cluster everywhere_dense -> dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
b1 is dense
proof end;
cluster non dense -> non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is dense holds
not b1 is everywhere_dense
proof end;
cluster non proper -> everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
b1 is everywhere_dense
proof end;
cluster non everywhere_dense -> proper SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is everywhere_dense holds
b1 is proper
proof end;
end;

registration
let X be non empty TopSpace;
cluster non empty strict dense everywhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th17: :: TEX_3:17  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 TopSpace
for A0 being non empty Subset of X st A0 is everywhere_dense holds
ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:18  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 TopSpace
for X0 being non empty everywhere_dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
proof end;

theorem :: TEX_3:19  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 TopSpace
for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
proof end;

theorem :: TEX_3:20  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 TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
proof end;

theorem :: TEX_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 non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
proof end;

theorem :: TEX_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1,the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
proof end;

registration
let X be non empty TopSpace;
cluster open dense -> dense everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is open holds
b1 is everywhere_dense
proof end;
cluster dense non everywhere_dense -> non open SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & not b1 is everywhere_dense holds
not b1 is open
proof end;
cluster open non everywhere_dense -> proper non dense non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & not b1 is everywhere_dense holds
not b1 is dense
proof end;
end;

registration
let X be non empty TopSpace;
cluster non empty strict open dense everywhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th23: :: TEX_3:23  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 TopSpace
for A0 being non empty Subset of X st A0 is dense & A0 is open holds
ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:24  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 TopSpace
for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds
X1 union X2 is dense SubSpace of X
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds
X1 union X2 is everywhere_dense SubSpace of X
proof end;

theorem :: TEX_3:27  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 TopSpace
for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds
X1 meet X2 is everywhere_dense SubSpace of X
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds
X1 meet X2 is dense SubSpace of X
proof end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is boundary means :Def3: :: TEX_3:def 3
for A being Subset of X st A = the carrier of IT holds
A is boundary;
end;

:: deftheorem Def3 defines boundary TEX_3:def 3 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is boundary iff for A being Subset of X st A = the carrier of IT holds
A is boundary );

theorem Th29: :: TEX_3:29  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 TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
proof end;

registration
let X be non empty TopSpace;
cluster non empty open -> non empty non boundary SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is open holds
not b1 is boundary
proof end;
cluster non empty boundary -> non empty non open SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is open
proof end;
cluster everywhere_dense -> non boundary SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is boundary
proof end;
cluster boundary -> proper non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary holds
not b1 is everywhere_dense
proof end;
end;

theorem :: TEX_3:30  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 TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof end;

theorem Th31: :: TEX_3:31  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 TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is dense iff X2 is boundary )
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is boundary iff X2 is dense ) by Th31;

theorem Th33: :: TEX_3:33  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 TopSpace
for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
proof end;

theorem Th34: :: TEX_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 non empty TopSpace
for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary
proof end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is nowhere_dense means :Def4: :: TEX_3:def 4
for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense;
end;

:: deftheorem Def4 defines nowhere_dense TEX_3:def 4 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense );

theorem Th35: :: TEX_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 non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
proof end;

registration
let X be non empty TopSpace;
cluster nowhere_dense -> proper non everywhere_dense boundary SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is nowhere_dense holds
b1 is boundary
proof end;
cluster non boundary -> non nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is boundary holds
not b1 is nowhere_dense
proof end;
cluster nowhere_dense -> proper non dense non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is nowhere_dense holds
not b1 is dense
proof end;
cluster dense -> non nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense holds
not b1 is nowhere_dense
proof end;
end;

theorem :: TEX_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 non empty TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 )
proof end;

theorem Th37: :: TEX_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 TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is everywhere_dense iff X2 is nowhere_dense )
proof end;

theorem :: TEX_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 TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is nowhere_dense iff X2 is everywhere_dense ) by Th37;

theorem Th39: :: TEX_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 TopSpace
for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
proof end;

theorem Th40: :: TEX_3:40  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 TopSpace
for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense
proof end;

registration
let X be non empty TopSpace;
cluster closed boundary -> proper non dense non everywhere_dense boundary nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary & b1 is closed holds
b1 is nowhere_dense
proof end;
cluster boundary non nowhere_dense -> non closed SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary & not b1 is nowhere_dense holds
not b1 is closed
proof end;
cluster closed non nowhere_dense -> non boundary non nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed & not b1 is nowhere_dense holds
not b1 is boundary
proof end;
end;

theorem Th41: :: TEX_3:41  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 TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof end;

theorem :: TEX_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 TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
proof end;

theorem :: TEX_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 TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds
X1 meet X2 is boundary
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds
X1 union X2 is nowhere_dense
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds
X1 union X2 is boundary
proof end;

theorem :: TEX_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 non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds
X1 meet X2 is nowhere_dense
proof end;

theorem :: TEX_3:47  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 TopSpace st ( for X0 being SubSpace of X holds not X0 is boundary ) holds
X is discrete
proof end;

theorem :: TEX_3:48  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 non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is dense ) holds
X is discrete
proof end;

registration
let X be non empty discrete TopSpace;
cluster non empty -> non empty non boundary non nowhere_dense SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds not b1 is boundary ;
cluster proper -> proper non dense non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is dense
proof end;
cluster dense -> non proper dense everywhere_dense non boundary non nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense holds
not b1 is proper
proof end;
end;

registration
let X be non empty discrete TopSpace;
cluster non empty strict non boundary non nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is boundary & b1 is strict & not b1 is empty )
proof end;
end;

registration
let X be non empty discrete non trivial TopSpace;
cluster strict proper non dense non everywhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is dense & b1 is strict )
proof end;
end;

theorem :: TEX_3:49  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 TopSpace st ex X0 being non empty SubSpace of X st X0 is boundary holds
not X is discrete
proof end;

theorem :: TEX_3:50  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 TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is proper ) holds
not X is discrete
proof end;

registration
let X be non empty non discrete TopSpace;
cluster non empty strict non open proper non everywhere_dense boundary SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is boundary & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict non closed proper dense non nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem :: TEX_3:51  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 non discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:52  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 non discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense holds
ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:53  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 non discrete TopSpace
for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:54  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 non discrete TopSpace
for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:55  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 non discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1,the topology of Y1 #) holds
( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )
proof end;

theorem :: TEX_3:56  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 TopSpace st ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) holds
X is almost_discrete
proof end;

theorem :: TEX_3:57  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 non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) holds
X is almost_discrete
proof end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty -> non empty non nowhere_dense SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds not b1 is nowhere_dense
proof end;
cluster proper -> proper non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is everywhere_dense
proof end;
cluster everywhere_dense -> non proper dense everywhere_dense non boundary non nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is proper
proof end;
cluster non empty boundary -> non empty non closed SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is closed
proof end;
cluster non empty closed -> non empty non boundary non nowhere_dense SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is closed holds
not b1 is boundary
proof end;
cluster proper dense -> non open SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is open
proof end;
cluster open dense -> non proper dense everywhere_dense non boundary non nowhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is open holds
not b1 is proper
proof end;
cluster open proper -> proper non dense non everywhere_dense SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & b1 is proper holds
not b1 is dense
proof end;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict non nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof end;
end;

registration
let X be non empty almost_discrete non trivial TopSpace;
cluster strict proper non everywhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is everywhere_dense & b1 is strict )
proof end;
end;

theorem :: TEX_3:58  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 TopSpace st ex X0 being non empty SubSpace of X st X0 is nowhere_dense holds
not X is almost_discrete
proof end;

theorem :: TEX_3:59  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 TopSpace st ex X0 being non empty SubSpace of X st
( X0 is boundary & X0 is closed ) holds
not X is almost_discrete
proof end;

theorem :: TEX_3:60  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 TopSpace st ex X0 being non empty SubSpace of X st
( X0 is everywhere_dense & X0 is proper ) holds
not X is almost_discrete
proof end;

theorem :: TEX_3:61  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 TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is open & X0 is proper ) holds
not X is almost_discrete
proof end;

registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict non open proper non dense non everywhere_dense boundary nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict non closed proper dense everywhere_dense non boundary non nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th62: :: TEX_3:62  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 non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:63  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 non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is everywhere_dense holds
ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:64  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 non almost_discrete TopSpace
for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:65  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 non almost_discrete TopSpace
for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:66  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 non almost_discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1,the topology of Y1 #) holds
( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )
proof end;

registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict closed non open proper non dense non everywhere_dense boundary nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is boundary & b1 is closed & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict non closed open proper dense everywhere_dense non boundary non nowhere_dense SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th67: :: TEX_3:67  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 non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:68  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 non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:69  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 non almost_discrete TopSpace
for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:70  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 non almost_discrete TopSpace
for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:71  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 non almost_discrete TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
proof end;

theorem :: TEX_3:72  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 non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0,the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X,the topology of X #) ) )
proof end;

theorem :: TEX_3:73  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 non almost_discrete TopSpace
for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0,the topology of X0 #) ) )
proof end;

theorem :: TEX_3:74  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 non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
proof end;

theorem :: TEX_3:75  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 non almost_discrete TopSpace
for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
proof end;