:: CANTOR_1 semantic presentation

REAL is set
NAT is non trivial non finite countable denumerable set
bool NAT is non empty set
bool REAL is non empty set
NAT is non trivial non finite countable denumerable Element of bool REAL
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
{} is empty Function-like functional finite V42() countable set
the empty Function-like functional finite V42() countable set is empty Function-like functional finite V42() countable set
union {} is finite countable set
meet {} is set
dom {} is set
rng {} is set
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
P1 is Element of bool (bool T1)
P1 is Element of bool (bool T1)
P2 is Element of bool (bool T1)
x is Element of bool T1
c₆ is Element of bool (bool T1)
union c₆ is Element of bool T1
c₆ is Element of bool (bool T1)
union c₆ is Element of bool T1
T1 is TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
T1 is TopStruct
the topology of T1 is open Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
P1 is set
( the carrier of T1, the topology of T1) is Element of bool (bool the carrier of T1)
{P1} is non empty finite countable set
P2 is Element of bool (bool the carrier of T1)
union P2 is Element of bool the carrier of T1
T1 is TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
the topology of T1 is open (T1) Element of bool (bool the carrier of T1)
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
P1 is set
P2 is Element of bool T1
{P2} is non empty finite countable set
x is Element of bool (bool T1)
union x is Element of bool T1
T1 is TopStruct
the topology of T1 is open (T1) Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
T1 is TopStruct
the topology of T1 is open (T1) Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
P1 is Element of bool (bool T1)
P1 is Element of bool (bool T1)
P2 is Element of bool (bool T1)
x is Element of bool T1
c₆ is Element of bool (bool T1)
Intersect c₆ is Element of bool T1
c₆ is Element of bool (bool T1)
Intersect c₆ is Element of bool T1
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
P1 is set
P2 is Element of bool T1
{P2} is non empty finite countable set
x is Element of bool (bool T1)
meet x is Element of bool T1
Intersect x is Element of bool T1
T1 is non empty TopSpace-like TopStruct
the topology of T1 is non empty open (T1) Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
( the carrier of T1, the topology of T1) is Element of bool (bool the carrier of T1)
Fin the topology of T1 is preBoolean set
P1 is Element of Fin the topology of T1
meet P1 is set
P2 is Element of the topology of T1
{P2} is non empty finite countable set
P1 \/ {P2} is non empty set
meet (P1 \/ {P2}) is set
meet {P2} is set
(meet P1) /\ (meet {P2}) is set
{}. the topology of T1 is empty Function-like functional finite V42() countable Element of Fin the topology of T1
meet ({}. the topology of T1) is set
P1 is Element of bool the carrier of T1
P2 is Element of bool (bool the carrier of T1)
Intersect P2 is Element of bool the carrier of T1
x is Element of bool (bool the carrier of T1)
meet x is Element of bool the carrier of T1
x is Element of bool (bool the carrier of T1)
bool the carrier of T1 is non empty Element of bool (bool the carrier of T1)
{} (bool the carrier of T1) is empty proper Function-like functional finite V42() countable Element of bool (bool the carrier of T1)
bool (bool the carrier of T1) is non empty set
c₆ is Element of bool (bool the carrier of T1)
Intersect c₆ is Element of bool the carrier of T1
x is Element of bool (bool the carrier of T1)
T1 is TopSpace-like TopStruct
the topology of T1 is non empty open (T1) Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
( the carrier of T1, the topology of T1) is Element of bool (bool the carrier of T1)
T2 is set
P1 is Element of bool the carrier of T1
P2 is Element of bool (bool the carrier of T1)
union P2 is Element of bool the carrier of T1
T1 is non empty TopSpace-like TopStruct
the topology of T1 is non empty open (T1) Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
( the carrier of T1, the topology of T1) is Element of bool (bool the carrier of T1)
( the carrier of T1,( the carrier of T1, the topology of T1)) is Element of bool (bool the carrier of T1)
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
P1 is Element of bool (bool T1)
Intersect P1 is Element of bool T1
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
P1 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
(T1,P1) is Element of bool (bool T1)
P2 is set
x is Element of bool T1
c₆ is Element of bool (bool T1)
union c₆ is Element of bool T1
T1 is set
bool T1 is non empty Element of bool (bool T1)
bool T1 is non empty set
bool (bool T1) is non empty set
bool (bool T1) is non empty set
bool (bool (bool T1)) is non empty set
T2 is non empty Element of bool (bool (bool T1))
{ (Intersect b₁) where b₁ is Element of T2 : verum } is set
union T2 is Element of bool (bool T1)
Intersect (union T2) is Element of bool T1
P1 is Element of bool (bool T1)
Intersect P1 is Element of bool T1
P2 is set
x is set
c₆ is set
G is Element of bool (bool T1)
B is Element of bool (bool T1)
Intersect B is Element of bool T1
P2 is set
x is set
c₆ is Element of T2
Intersect c₆ is Element of bool T1
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
(T1,(T1,T2)) is Element of bool (bool T1)
P1 is set
P2 is Element of bool T1
x is Element of bool (bool T1)
Intersect x is Element of bool T1
bool T2 is non empty Element of bool (bool T2)
bool T2 is non empty set
bool (bool T2) is non empty set
c₆ is set
G is Element of bool T1
B is Element of bool (bool T1)
Intersect B is Element of bool T1
[:x,(bool T2):] is set
bool [:x,(bool T2):] is non empty set
c₆ is Relation-like x -defined bool T2 -valued Function-like V21(x, bool T2) Element of bool [:x,(bool T2):]
rng c₆ is set
{ (Intersect b₁) where b₁ is Element of bool (bool T1) : b₁ in rng c₆ } is set
B is set
V is Element of bool (bool T1)
Intersect V is Element of bool T1
dom c₆ is set
V is set
c₆ . V is Element of bool (bool T1)
x is Element of bool (bool T1)
Intersect x is Element of bool T1
union (rng c₆) is set
union (bool T2) is Element of bool T2
B is Element of bool (bool T1)
V is set
c₆ . V is Element of bool (bool T1)
x is Element of bool (bool T1)
Intersect x is Element of bool T1
dom c₆ is set
V is Element of bool (bool T1)
Intersect V is Element of bool T1
bool T1 is non empty Element of bool (bool T1)
bool (bool T1) is non empty Element of bool (bool (bool T1))
bool (bool T1) is non empty set
bool (bool (bool T1)) is non empty set
V is non empty Element of bool (bool (bool T1))
x is non empty Element of bool (bool (bool T1))
{ (Intersect b₁) where b₁ is Element of x : verum } is set
x is set
G is Element of bool (bool T1)
Intersect G is Element of bool T1
x is set
G is Element of x
Intersect G is Element of bool T1
dom c₆ is set
V is set
dom c₆ is set
x is set
c₆ . x is Element of bool (bool T1)
x is Element of bool T1
c₆ . x is Element of bool (bool T1)
G is Element of bool (bool T1)
c₁₄ is Element of bool (bool T1)
Intersect c₁₄ is Element of bool T1
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
P1 is set
P2 is set
P1 /\ P2 is set
{P1,P2} is non empty finite countable set
x is Element of bool (bool T1)
c₆ is Element of bool (bool T1)
meet c₆ is Element of bool T1
Intersect c₆ is Element of bool T1
(T1,(T1,T2)) is Element of bool (bool T1)
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
P1 is set
P2 is set
INTERSECTION (P1,P2) is set
x is set
c₆ is set
G is set
c₆ /\ G is set
{c₆,G} is non empty finite countable set
B is Element of bool (bool T1)
V is Element of bool (bool T1)
meet V is Element of bool T1
Intersect V is Element of bool T1
(T1,(T1,T2)) is Element of bool (bool T1)
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
P1 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
(T1,P1) is Element of bool (bool T1)
P2 is set
x is Element of bool T1
c₆ is Element of bool (bool T1)
Intersect c₆ is Element of bool T1
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
T1 is non empty set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is non empty Element of bool (bool T1)
(T1,(T1,T2)) is Element of bool (bool T1)
TopStruct(# T1,(T1,(T1,T2)) #) is non empty strict TopStruct
[#] TopStruct(# T1,(T1,(T1,T2)) #) is Element of bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)
the carrier of TopStruct(# T1,(T1,(T1,T2)) #) is set
bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #) is non empty set
{([#] TopStruct(# T1,(T1,(T1,T2)) #))} is non empty finite countable set
P2 is Element of bool (bool T1)
x is Element of bool (bool T1)
c₆ is Element of bool (bool T1)
union c₆ is Element of bool T1
the topology of TopStruct(# T1,(T1,(T1,T2)) #) is open ( TopStruct(# T1,(T1,(T1,T2)) #)) Element of bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #))
bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)) is non empty set
P2 is Element of bool (bool T1)
union P2 is Element of bool T1
P2 is Element of bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #))
union P2 is Element of bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)
bool (T1,T2) is non empty set
bool (bool (T1,T2)) is non empty set
x is Element of bool (bool (T1,T2))
{ (union b₁) where b₁ is Element of bool (T1,T2) : b₁ in x } is set
G is set
B is Element of bool T1
V is Element of bool (bool T1)
union V is Element of bool T1
G is set
B is Element of bool (T1,T2)
union B is set
V is Element of bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)
union x is Element of bool (T1,T2)
union (union x) is set
union { (union b₁) where b₁ is Element of bool (T1,T2) : b₁ in x } is set
bool T1 is non empty Element of bool (bool T1)
P2 is Element of bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)
x is Element of bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)
P2 /\ x is Element of bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)
c₆ is Element of bool (bool T1)
union c₆ is Element of bool T1
G is Element of bool (bool T1)
union G is Element of bool T1
INTERSECTION (c₆,G) is set
union (INTERSECTION (c₆,G)) is set
T1 is TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
T1 is TopStruct
the topology of T1 is open (T1) Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
( the carrier of T1, the topology of T1) is non empty Element of bool (bool the carrier of T1)
T2 is open (T1) Element of bool (bool the carrier of T1)
( the carrier of T1,T2) is non empty Element of bool (bool the carrier of T1)
T1 is non empty set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is Element of bool (bool T1)
TopStruct(# T1,(T1,T2) #) is non empty strict TopStruct
the carrier of TopStruct(# T1,(T1,T2) #) is set
bool the carrier of TopStruct(# T1,(T1,T2) #) is non empty set
bool (bool the carrier of TopStruct(# T1,(T1,T2) #)) is non empty set
T1 is non empty strict TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
T2 is non empty strict TopSpace-like TopStruct
the carrier of T2 is set
bool the carrier of T2 is non empty set
bool (bool the carrier of T2) is non empty set
P1 is open (T1) Element of bool (bool the carrier of T1)
( the carrier of T1,P1) is non empty Element of bool (bool the carrier of T1)
x is open (T1) (T1) Element of bool (bool the carrier of T1)
the topology of T1 is non empty open (T1) (T1) Element of bool (bool the carrier of T1)
( the carrier of T1, the topology of T1) is non empty Element of bool (bool the carrier of T1)
( the carrier of T1,( the carrier of T1,P1)) is Element of bool (bool the carrier of T1)
( the carrier of T1,( the carrier of T1, the topology of T1)) is Element of bool (bool the carrier of T1)
P2 is open (T2) Element of bool (bool the carrier of T2)
the topology of T2 is non empty open (T2) (T2) Element of bool (bool the carrier of T2)
( the carrier of T2,P2) is non empty Element of bool (bool the carrier of T2)
( the carrier of T2, the topology of T2) is non empty Element of bool (bool the carrier of T2)
( the carrier of T2,( the carrier of T2,P2)) is Element of bool (bool the carrier of T2)
( the carrier of T2,( the carrier of T2, the topology of T2)) is Element of bool (bool the carrier of T2)
( the carrier of T1,x) is Element of bool (bool the carrier of T1)
c₆ is open (T2) (T2) Element of bool (bool the carrier of T2)
( the carrier of T2,c₆) is Element of bool (bool the carrier of T2)
T1 is non empty set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool T1)
(T1,T2) is non empty Element of bool (bool T1)
(T1,(T1,T2)) is Element of bool (bool T1)
TopStruct(# T1,(T1,(T1,T2)) #) is non empty strict TopStruct
the carrier of TopStruct(# T1,(T1,(T1,T2)) #) is set
bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #) is non empty set
bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #)) is non empty set
P2 is Element of bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #))
the topology of TopStruct(# T1,(T1,(T1,T2)) #) is open ( TopStruct(# T1,(T1,(T1,T2)) #)) ( TopStruct(# T1,(T1,(T1,T2)) #)) Element of bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #))
( the carrier of TopStruct(# T1,(T1,(T1,T2)) #),P2) is non empty Element of bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #))
x is open ( TopStruct(# T1,(T1,(T1,T2)) #)) ( TopStruct(# T1,(T1,(T1,T2)) #)) Element of bool (bool the carrier of TopStruct(# T1,(T1,(T1,T2)) #))
0 is empty Function-like functional finite V42() countable Element of NAT
1 is non empty set
{0,1} is non empty finite countable set
NAT --> {0,1} is non trivial Relation-like non-empty NAT -defined {{0,1}} -valued Function-like constant V17( NAT ) V21( NAT ,{{0,1}}) non finite Element of bool [:NAT,{{0,1}}:]
{{0,1}} is non empty finite V42() countable set
[:NAT,{{0,1}}:] is set
bool [:NAT,{{0,1}}:] is non empty set
product (NAT --> {0,1}) is non empty functional with_common_domain product-like set
bool (product (NAT --> {0,1})) is non empty set
bool (bool (product (NAT --> {0,1}))) is non empty set
T1 is Element of bool (bool (product (NAT --> {0,1})))
((product (NAT --> {0,1})),T1) is non empty Element of bool (bool (product (NAT --> {0,1})))
((product (NAT --> {0,1})),((product (NAT --> {0,1})),T1)) is Element of bool (bool (product (NAT --> {0,1})))
TopStruct(# (product (NAT --> {0,1})),((product (NAT --> {0,1})),((product (NAT --> {0,1})),T1)) #) is non empty strict TopStruct
T2 is non empty strict TopSpace-like TopStruct
the carrier of T2 is set
bool the carrier of T2 is non empty set
bool (bool the carrier of T2) is non empty set
P1 is open (T2) Element of bool (bool the carrier of T2)
P2 is functional with_common_domain Element of bool (product (NAT --> {0,1}))
x is functional with_common_domain Element of bool (product (NAT --> {0,1}))
c₆ is V37() set
G is V37() set
T1 is non empty strict TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
T2 is non empty strict TopSpace-like TopStruct
the carrier of T2 is set
bool the carrier of T2 is non empty set
bool (bool the carrier of T2) is non empty set
P1 is open (T1) Element of bool (bool the carrier of T1)
P1 is open (T1) Element of bool (bool the carrier of T1)
P2 is open (T2) Element of bool (bool the carrier of T2)
P2 is open (T2) Element of bool (bool the carrier of T2)
x is functional with_common_domain Element of bool (product (NAT --> {0,1}))
c₆ is V37() set
G is V37() set
c₆ is V37() set
G is V37() set
() is non empty strict TopSpace-like TopStruct