:: 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

union c

c

union c

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

Intersect c

c

Intersect c

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

Intersect c

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

union c

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

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

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

Intersect c

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

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

rng c

{ (Intersect b

B is set

V is Element of bool (bool T1)

Intersect V is Element of bool T1

dom c

V is set

c

x is Element of bool (bool T1)

Intersect x is Element of bool T1

union (rng c

union (bool T2) is Element of bool T2

B is Element of bool (bool T1)

V is set

c

x is Element of bool (bool T1)

Intersect x is Element of bool T1

dom c

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

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

V is set

dom c

x is set

c

x is Element of bool T1

c

G is Element of bool (bool T1)

c

Intersect c

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

meet c

Intersect c

(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

G is set

c

{c

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

Intersect c

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

union c

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

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

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

union c

G is Element of bool (bool T1)

union G is Element of bool T1

INTERSECTION (c

union (INTERSECTION (c

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

( the carrier of T2,c

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

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

G is V37() set

c

G is V37() set

() is non empty strict TopSpace-like TopStruct