:: PENCIL_1 semantic presentation

REAL is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
2 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive Element of NAT
[:2,2:] is non empty finite countable set
[:[:2,2:],2:] is non empty finite countable set
bool [:[:2,2:],2:] is non empty finite V33() countable set
K255() is set

is non empty trivial finite V33() 1 -element countable set
1 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive Element of NAT
K233() is M11()
is set
bool is non empty set
K36(K233(),) is set

RAT is set
INT is set
{{},1} is non empty finite V33() countable set
3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive Element of NAT

{0,1,2} is non empty finite countable Element of bool NAT

dom A is set
rng A is set
S is set
A . S is set
rng I is set
dom I is set
S is set
I . S is set
I is set
card I is V21() V22() V23() cardinal set
card 2 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

dom A is set
rng A is set
A . 0 is set
S is set
A . 1 is set
B is set
A is set
S is set
{A,S} is non empty finite countable set
B is set
card {A,S} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is set
card I is V21() V22() V23() cardinal set
A is set
S is set
B is set
I is set
card I is V21() V22() V23() cardinal set
the Element of I is Element of I
S is set
B is set
l is set
{l} is non empty trivial finite 1 -element countable set
{ the Element of I} is non empty trivial finite 1 -element countable set
S is set
I is set
card I is V21() V22() V23() cardinal set
card 3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

dom A is set
rng A is set
A . 0 is set
S is set
A . 1 is set
B is set
A . 2 is set
l is set
A is set
S is set
B is set
{A,S,B} is non empty finite countable set
l is set
card {A,S,B} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is set
card I is V21() V22() V23() cardinal set
A is set
S is set
B is set
l is set
L is set
I is TopStruct
the carrier of I is set
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
I is non empty set
card I is non empty V21() V22() V23() cardinal set
bool I is non empty set
{ b1 where b1 is Element of bool I : 2 = card b1 } is set
A is set
S is set
{A,S} is non empty finite countable set
B is set
l is TopStruct
the carrier of l is set
the topology of l is Element of bool (bool the carrier of l)
bool the carrier of l is non empty set
bool (bool the carrier of l) is non empty set
B is Element of bool I
card B is V21() V22() V23() cardinal set
L is non empty set
a is Element of bool I
card a is V21() V22() V23() cardinal set
a is Element of the carrier of l
b is Element of the carrier of l
L is set
{a,b} is non empty finite countable set
a1 is Element of the carrier of l
{a,a1} is non empty finite countable set
b1 is set
b1 is set
b1 is Element of bool I
card b1 is V21() V22() V23() cardinal set
{a,b} is non empty finite countable set
L is set
card {a,b} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L is Element of bool I
a is Element of the topology of l
card a is V21() V22() V23() cardinal set
b is Element of bool I
card b is V21() V22() V23() cardinal set
a is Element of the topology of l
b is Element of the topology of l
a /\ b is set
card (a /\ b) is V21() V22() V23() cardinal set
L is set
a1 is set
{L,a1} is non empty finite countable set
b1 is set
a is Element of bool I
card a is V21() V22() V23() cardinal set

C is Element of bool I
card C is V21() V22() V23() cardinal set
card {L,a1} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

C is Element of bool I
card C is V21() V22() V23() cardinal set
C is Element of bool I
card C is V21() V22() V23() cardinal set
a is Element of the carrier of l
b is set
{a,b} is non empty finite countable set
L is set
card {a,b} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L is Element of bool I
a1 is Element of the topology of l
I is non empty set
card I is non empty V21() V22() V23() cardinal set
bool I is non empty set
{ b1 where b1 is Element of bool I : 2 = card b1 } is set
A is Element of bool I
card A is V21() V22() V23() cardinal set
{A} is non empty trivial finite 1 -element countable Element of bool (bool I)
bool (bool I) is non empty set
{ b1 where b1 is Element of bool I : 2 = card b1 } \ {A} is Element of bool { b1 where b1 is Element of bool I : 2 = card b1 }
bool { b1 where b1 is Element of bool I : 2 = card b1 } is non empty set

B is set
l is set
{B,l} is non empty finite countable set
L is TopStruct
the carrier of L is set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
a is Element of the carrier of L
b is Element of the carrier of L
L is set
{a,L} is non empty finite countable set
a1 is set
a1 is Element of bool I
card a1 is V21() V22() V23() cardinal set
b1 is non empty set
a is Element of bool I
card a is V21() V22() V23() cardinal set
{a,b} is non empty finite countable set
a is Element of the topology of L
C is Element of bool I
card C is V21() V22() V23() cardinal set

Li is set
o is set
{Li,o} is non empty finite countable set
a is Element of the topology of L
card a is V21() V22() V23() cardinal set
C is Element of bool I
card C is V21() V22() V23() cardinal set
a is Element of the topology of L
C is Element of the topology of L
a /\ C is set
card (a /\ C) is V21() V22() V23() cardinal set
j is set
Li is set
{j,Li} is non empty finite countable set
o is set
L1 is Element of bool I
card L1 is V21() V22() V23() cardinal set

L2 is Element of bool I
card L2 is V21() V22() V23() cardinal set
card {j,Li} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

L2 is Element of bool I
card L2 is V21() V22() V23() cardinal set
L2 is Element of bool I
card L2 is V21() V22() V23() cardinal set
a is Element of the carrier of L
C is set
{a,C} is non empty finite countable set
j is set
card {a,C} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
j is Element of bool I
Li is Element of the topology of L
C is set
{a,C} is non empty finite countable set
j is set
card {a,C} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
j is Element of bool I
Li is Element of the topology of L
bool 3 is non empty finite V33() countable set
{ b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } is set
I is set

card A is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
bool (bool 3) is non empty finite V33() countable set
I is finite V33() countable Element of bool (bool 3)
TopStruct(# 3,I #) is strict TopStruct
card 3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
card 2 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
bool 3 is non empty finite V33() countable set

card I is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
{ b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } is set
A is set

card S is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
bool (bool 3) is non empty finite V33() countable set
{I} is non empty trivial finite V33() 1 -element countable Element of bool (bool 3)
{ b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } \ {I} is Element of bool { b1 where b1 is finite countable Element of bool 3 : 2 = card b1 }
bool { b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } is non empty set
A is finite V33() countable Element of bool (bool 3)
TopStruct(# 3,A #) is strict TopStruct
card 3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is () TopStruct
the topology of I is Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
I is () TopStruct
the carrier of I is set
A is Element of the carrier of I
S is Element of the carrier of I
the topology of I is Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
{A,S} is non empty finite countable set
B is Element of the topology of I
B is Element of the topology of I

A is set
dom I is set
I . A is set
rng I is set
I is set
the TopStruct is TopStruct
I --> the TopStruct is Relation-like I -defined { the TopStruct } -valued Function-like constant V14(I) V18(I,{ the TopStruct }) 1-sorted-yielding Element of bool [:I,{ the TopStruct }:]
{ the TopStruct } is non empty trivial finite 1 -element countable set
[:I,{ the TopStruct }:] is set
bool [:I,{ the TopStruct }:] is non empty set
S is set
rng (I --> the TopStruct ) is set

rng I is set
A is set
A is TopStruct

A is 1-sorted
rng I is set

rng I is set
A is set
dom I is set
S is set
I . S is set
A is 1-sorted
I is non empty set

S is Element of I
A . S is set
dom A is set
A . S is 1-sorted
rng A is set

A is 1-sorted
rng I is set
A is set
rng I is set

A is set
rng I is set

A is set
rng I is set
S is non empty () () TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
B is set
l is Element of the topology of S
card l is V21() V22() V23() cardinal set
L is set
a is set
I is set
the non empty () () () () TopStruct is non empty () () () () TopStruct
I --> the non empty () () () () TopStruct is Relation-like I -defined { the non empty () () () () TopStruct } -valued Function-like constant V14(I) V18(I,{ the non empty () () () () TopStruct }) 1-sorted-yielding Element of bool [:I,{ the non empty () () () () TopStruct }:]
{ the non empty () () () () TopStruct } is non empty trivial finite 1 -element countable set
[:I,{ the non empty () () () () TopStruct }:] is set
bool [:I,{ the non empty () () () () TopStruct }:] is non empty set
S is set
rng (I --> the non empty () () () () TopStruct ) is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
S is Element of I
A . S is set
dom A is set
(I,A,S) is TopStruct
rng A is set
I is set
I is set

S is set
rng {A} is V33() set
dom {A} is set
B is set

A . B is set
{(A . B)} is non empty trivial finite 1 -element countable set
I is non empty set

S is Element of I
B is non empty non trivial set
A +* (S,B) is Relation-like I -defined Function-like V14(I) set
(A +* (S,B)) . S is set
l is set
rng (A +* (S,B)) is set
dom A is set
dom (A +* (S,B)) is set
I is non empty set

the Element of I is Element of I
B is Element of I

A . B is set
{(A . B)} is non empty trivial finite 1 -element countable set
I is non empty set

S is set
B is set
{A} +* (S,B) is Relation-like I -defined Function-like V14(I) set
dom {A} is set
l is Element of I
L is Element of I
({A} +* (S,B)) . L is set

A . L is set
{(A . L)} is non empty trivial finite 1 -element countable set
I is non empty set

B is set

() . B is set
l is Element of I
dom A is set
A . l is 1-sorted
rng A is set
S . l is set
() . l is set
the carrier of (A . l) is set
{(S . l)} is non empty trivial finite 1 -element countable set

I is non empty set

{} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set

I is non empty set

the Element of I is Element of I
A . the Element of I is 1-sorted
() . the Element of I is set
the carrier of (A . the Element of I) is set
the Relation-like I -defined Function-like V14(I) Element of Carrier A . the Element of I is set
L is 1-sorted
the carrier of L is set
dom A is set
rng A is set
a is non empty non trivial set
card the carrier of (A . the Element of I) is V21() V22() V23() cardinal set
b is Element of a
L is Element of a
l is Element of the carrier of (A . the Element of I)
b is set

L is Element of the carrier of (A . the Element of I)
L +* ( the Element of I,L) is Relation-like I -defined Function-like V14(I) set
b1 is set
(L +* ( the Element of I,L)) . b1 is set
() . b1 is set
L . b1 is set
dom L is set
a is 1-sorted
the carrier of a is set
{L,(L +* ( the Element of I,L))} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set
b1 is set
{L,(L +* ( the Element of I,L))} . b1 is finite countable set
() . b1 is set
a is Element of I
A . a is 1-sorted
L . a is set
() . a is set
the carrier of (A . a) is set
(L +* ( the Element of I,L)) . a is set
{(L . a),((L +* ( the Element of I,L)) . a)} is non empty finite countable set
{L,(L +* ( the Element of I,L))} . a is finite countable set
dom L is set
(L +* ( the Element of I,L)) . the Element of I is set

b1 . the Element of I is set
{l,L} is non empty finite countable set
a is set
{a} is non empty trivial finite 1 -element countable set
a is Element of I
b1 . a is set
L . a is set
(L +* ( the Element of I,L)) . a is set
{(L . a),(L . a)} is non empty finite countable set
{(L . a)} is non empty trivial finite 1 -element countable set
dom b1 is set
rng b1 is set
I is non empty set

the Element of I is Element of I
{} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set
{0,1} is non empty finite V33() countable Element of bool NAT
{} +* ( the Element of I,{0,1}) is Relation-like I -defined Function-like V14(I) set

l is Element of I
B . l is set
{} . l is finite countable set
dom {} is set
rng {} is V33() set
B . the Element of I is set
l is set
rng B is set
dom B is set
dom {} is set
card {0,1} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is non empty set
A is Relation-like I -defined Function-like V14(I) () (I) set
S is Element of I
A . S is set
rng A is set
B is set
dom A is set
l is set
A . l is set
L is Element of I
L is Element of I
A . L is set
L is Element of I
S is Element of I
A . S is set
B is Element of I
A . B is set
l is Element of I
I is non empty set
A is Relation-like I -defined Function-like V14(I) () (I) set
(I,A) is Element of I
S is Element of I
A . S is set
B is Element of I
A . (I,A) is set
I is non empty set

S is Relation-like I -defined Function-like V14(I) () (I) set
rng S is set
dom A is set
B is set
S . B is set
l is Element of I
(I,S) is Element of I
l is Element of I
(I,S) is Element of I
S . l is set
l is Element of I
(I,S) is Element of I
I is non empty set

card () is V21() V22() V23() cardinal set
dom A is set
S is set
B is set

dom l is set
L is set
A . L is set

dom L is set
a is set
L . a is set
l . a is set
A . a is set
rng A is set
card (A . a) is V21() V22() V23() cardinal set
rng A is set
S is set
B is set
A . B is set
B is set
l is set
A . l is set

dom L is set
card S is V21() V22() V23() cardinal set

a . l is set
b is set
L is Element of I
a +* (L,b) is Relation-like I -defined Function-like V14(I) set
b1 is set
(a +* (L,b)) . b1 is set
a . b1 is set
A . b1 is set
(a +* (L,b)) . b1 is set
A . b1 is set
dom (a +* (L,b)) is set
(a +* (L,b)) . L is set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set

S is set
dom A is set

dom l is set
(I,A) is Element of I
A . (I,A) is set
card (A . (I,A)) is V21() V22() V23() cardinal set

B . (I,A) is set
l is set
B +* ((I,A),l) is Relation-like I -defined Function-like V14(I) set
a is set
(B +* ((I,A),l)) . a is set
A . a is set
dom B is set
B . a is set

dom b is set
dom B is set
(B +* ((I,A),l)) . (I,A) is set
dom (B +* ((I,A),l)) is set
card () is non empty V21() V22() V23() cardinal set
I is non empty set

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
S is set
B is set
B is Element of bool (bool (product ()))
l is set

a is set
dom L is set

dom b is set
dom () is set
L is set
b . L is set
() . L is set
L . L is set
a is Element of I
L . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
S is Element of bool (bool (product ()))
B is Element of bool (bool (product ()))
l is set

a is Element of I
L . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set

a is Element of I
L . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
I is non empty set

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
I is non empty set

(I,A) is non empty TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
the carrier of (I,A) is non empty set
S is Element of the carrier of (I,A)
dom () is set

dom B is set
I is non empty set

(I,A) is non empty TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct

B is Element of I
(I,A,B) is TopStruct
the topology of (I,A,B) is Element of bool (bool the carrier of (I,A,B))
the carrier of (I,A,B) is set
bool the carrier of (I,A,B) is non empty set
bool (bool the carrier of (I,A,B)) is non empty set
the Element of the topology of (I,A,B) is Element of the topology of (I,A,B)
the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A +* (B, the Element of the topology of (I,A,B)) is Relation-like I -defined Function-like V14(I) set
L is set
( the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A +* (B, the Element of the topology of (I,A,B))) . L is set
() . L is set

A . L is set
a is 1-sorted
the carrier of a is set

L is Element of I
( the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A +* (B, the Element of the topology of (I,A,B))) . L is set

L . B is set

I is non empty set

(I,A) is non empty TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
S is Element of I
(I,A,S) is TopStruct
S is non empty set

l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
() . l is set
L is 1-sorted
the carrier of L is set
L is Element of I
(I,A,L) is TopStruct
I is non empty set

(I,A) is non empty TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
the topology of (I,A) is Element of bool (bool the carrier of (I,A))
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
bool (bool the carrier of (I,A)) is non empty set
S is Element of the topology of (I,A)
card S is V21() V22() V23() cardinal set
B is Element of I
(I,A,B) is TopStruct

l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
L is Element of I
(I,A,L) is TopStruct
card (B . l) is V21() V22() V23() cardinal set
dom B is set
rng B is set
L is Relation-like non-empty I -defined Function-like V14(I) () (I) set

I is non empty set

(I,A) is non empty TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
the topology of (I,A) is Element of bool (bool the carrier of (I,A))
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
bool (bool the carrier of (I,A)) is non empty set
S is Element of the topology of (I,A)
B is Element of the topology of (I,A)
S /\ B is set
card (S /\ B) is V21() V22() V23() cardinal set
l is set
L is set
a is Element of I
(I,A,a) is TopStruct

dom b is set
dom a is set
a1 is Element of I
a . a1 is set
(I,A,a1) is TopStruct
the topology of (I,A,a1) is Element of bool (bool the carrier of (I,A,a1))
the carrier of (I,A,a1) is set
bool the carrier of (I,A,a1) is non empty set
bool (bool the carrier of (I,A,a1)) is non empty set
a1 is Element of I
a . a1 is set
(I,A,a1) is TopStruct
the topology of (I,A,a1) is Element of bool (bool the carrier of (I,A,a1))
the carrier of (I,A,a1) is set
bool the carrier of (I,A,a1) is non empty set
bool (bool the carrier of (I,A,a1)) is non empty set
b1 is Element of I
a . b1 is set
a is Element of I
C is Element of I
(I,A,C) is TopStruct
card (a . a1) is V21() V22() V23() cardinal set
b1 is Element of I
(I,A,b1) is TopStruct
b1 is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A

dom b1 is set
a is Element of I
b1 . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
a is Element of I
b1 . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set

dom C is set

Li is set
j . Li is set
L . Li is set
o is Element of I
L . o is set
a . o is set
j . o is set
card (a . o) is V21() V22() V23() cardinal set
b1 . o is set
L1 is Element of I
b1 . L1 is set
L2 is Element of I
L3 is Element of I
(I,A,L3) is TopStruct
card (b1 . a) is V21() V22() V23() cardinal set
card (b1 . o) is V21() V22() V23() cardinal set
L1 is set
a . L1 is set
b1 . L1 is set
L2 is Element of I
(I,A,L2) is TopStruct
the topology of (I,A,L2) is Element of bool (bool the carrier of (I,A,L2))
the carrier of (I,A,L2) is set
bool the carrier of (I,A,L2) is non empty set
bool (bool the carrier of (I,A,L2)) is non empty set
b1 . L2 is set
a . L2 is set
j . L2 is set
x is Element of the topology of (I,A,L2)
L3 is Element of the topology of (I,A,L2)
x /\ L3 is set
L . L2 is set
card (x /\ L3) is V21() V22() V23() cardinal set
y is Element of I
(I,A,y) is TopStruct
L2 is Element of I
a . L2 is set
L3 is set
{L3} is non empty trivial finite 1 -element countable set
j . L2 is set
b1 . L2 is set
L2 is Element of I
L1 is set
b1 . L1 is set
a . L1 is set
L2 is Element of I
(I,A,L2) is TopStruct
the topology of (I,A,L2) is Element of bool (bool the carrier of (I,A,L2))
the carrier of (I,A,L2) is set
bool the carrier of (I,A,L2) is non empty set
bool (bool the carrier of (I,A,L2)) is non empty set
b1 . L2 is set
a . L2 is set
j . L2 is set
x is Element of the topology of (I,A,L2)
L3 is Element of the topology of (I,A,L2)
x /\ L3 is set
L . L2 is set
card (x /\ L3) is V21() V22() V23() cardinal set
y is Element of I
(I,A,y) is TopStruct
L2 is Element of I
b1 . L2 is set
L3 is set
{L3} is non empty trivial finite 1 -element countable set
j . L2 is set
a . L2 is set
L2 is Element of I
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
S is Element of I
(I,A,S) is non empty () () () () TopStruct
B is Element of I
(I,A,B) is non empty () () () () TopStruct
the Element of I is Element of I
(I,A, the Element of I) is non empty () () () () TopStruct
S is Element of I
(I,A,S) is non empty () () () () TopStruct
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
A is Element of bool the carrier of I
S is Element of the carrier of I
B is Element of the carrier of I
card A is V21() V22() V23() cardinal set
the topology of I is Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
S is Element of the topology of I
S /\ A is Element of bool the carrier of I
card (S /\ A) is V21() V22() V23() cardinal set
card A is V21() V22() V23() cardinal set
I is () TopStruct
the topology of I is Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
A is Element of the topology of I
S is Element of bool the carrier of I
B is Element of the topology of I
B /\ S is Element of bool the carrier of I
card (B /\ S) is V21() V22() V23() cardinal set
I is TopStruct
the topology of I is Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
A is Element of the topology of I
S is Element of bool the carrier of I
B is Element of the carrier of I
l is Element of the carrier of I
{B,l} is non empty finite countable set
I is () TopStruct
[#] I is non proper Element of bool the carrier of I
the carrier of I is set
bool the carrier of I is non empty set
the topology of I is non empty Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
A is Element of the topology of I
A /\ ([#] I) is Element of bool the carrier of I
card (A /\ ([#] I)) is V21() V22() V23() cardinal set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set

(I,A) is Element of I

l is set
S . l is set
B . l is set
dom A is set
dom B is set
dom S is set
a is Element of I
A . (I,A) is set
L is Element of I
A . L is set
A . l is set
b is set
{b} is non empty trivial finite 1 -element countable set
S . L is set
B . L is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty () () () () TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
bool (bool the carrier of (I,A)) is non empty set
S is set

card () is V21() V22() V23() cardinal set

L is Element of I
B . L is set
(I,A,L) is non empty () () () () TopStruct
the topology of (I,A,L) is non empty Element of bool (bool the carrier of (I,A,L))
the carrier of (I,A,L) is non empty set
bool the carrier of (I,A,L) is non empty set
bool (bool the carrier of (I,A,L)) is non empty set
L is Element of I
l . L is set
(I,A,L) is non empty () () () () TopStruct
the topology of (I,A,L) is non empty Element of bool (bool the carrier of (I,A,L))
the carrier of (I,A,L) is non empty set
bool the carrier of (I,A,L) is non empty set
bool (bool the carrier of (I,A,L)) is non empty set
(I,l) is Element of I
card (l . L) is V21() V22() V23() cardinal set

(I,B) is Element of I
B . (I,B) is set
(I,A,(I,B)) is non empty () () () () TopStruct
the topology of (I,A,(I,B)) is non empty Element of bool (bool the carrier of (I,A,(I,B)))
the carrier of (I,A,(I,B)) is non empty set
bool the carrier of (I,A,(I,B)) is non empty set
bool (bool the carrier of (I,A,(I,B))) is non empty set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty () () () () TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
the carrier of (I,A) is non empty set

B is Element of I
(I,A,B) is non empty () () () () TopStruct
the carrier of (I,A,B) is non empty set
l is Element of the carrier of (I,A,B)
S +* (B,l) is Relation-like I -defined Function-like V14(I) set
dom () is set
L is set
(S +* (B,l)) . L is set
() . L is set
dom S is set
S . L is set
dom (S +* (B,l)) is set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set

S is Relation-like non-empty I -defined Function-like V14(I) () (I) set

() /\ () is set
card (() /\ ()) is V21() V22() V23() cardinal set
(I,A) is Element of I
(I,S) is Element of I
dom S is set
B is set
l is set
dom A is set

dom L is set

dom a is set
b is set
a . b is set
L . b is set
L is Element of I
L . L is set
S . L is set
a . L is set
card (S . L) is V21() V22() V23() cardinal set
A . L is set
card (A . L) is V21() V22() V23() cardinal set
a1 is set
A . a1 is set
S . a1 is set
b1 is set
{b1} is non empty trivial finite 1 -element countable set
a . a1 is set
a is set
{a} is non empty trivial finite 1 -element countable set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set
(I,A) is Element of I
S is non empty non trivial set
A +* ((I,A),S) is Relation-like I -defined Function-like V14(I) set
B is Element of I
(A +* ((I,A),S)) . B is set
A . B is set
(A +* ((I,A),S)) . (I,A) is set
rng (A +* ((I,A),S)) is set
dom (A +* ((I,A),S)) is set
dom A is set
I is non empty () () () TopStruct
the carrier of I is non empty set
A is Element of the carrier of I
S is Element of the carrier of I

len <*A*> is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

len <*S*> is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
the topology of I is non empty Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
B is Element of the topology of I
l is Element of bool the carrier of I

L . 1 is set
len L is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . (len L) is set
rng L is set

(len L) - 1 is V28() V186() ext-real set
a is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
b is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

len L is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

(len L) + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
rng L is set
a1 is set
L . a1 is set
b1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . b1 is set
L . b1 is set
b1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . (b1 + 1) is set
(L . b1) /\ (L . (b1 + 1)) is set
card (L . b1) is V21() V22() V23() cardinal set

a1 is set

dom a is set

dom C is set

rng ((<*A*> ^ a) ^ <*S*>) is set
C is set
rng (<*A*> ^ a) is set
rng <*S*> is set
(rng (<*A*> ^ a)) \/ () is set
rng <*A*> is set
rng a is set
() \/ (rng a) is set
{A} is non empty trivial finite 1 -element countable Element of bool the carrier of I

j is set
a . j is set
Li is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . Li is set
L . Li is set
Li + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . (Li + 1) is set
(L . Li) /\ (L . (Li + 1)) is set

dom o is set

dom o is set

dom o is set
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of I
len (<*A*> ^ a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
len a is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
() + (len a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(len a) + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

C . 1 is set
len C is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
C . (len C) is set

(len (<*A*> ^ a)) + () is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(len (<*A*> ^ a)) + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
j is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
C . j is set
j + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
C . (j + 1) is set
Li is Element of the carrier of I
o is Element of the carrier of I
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
len (a ^ <*S*>) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
len (<*A*> ^ (a ^ <*S*>)) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
() + (len (a ^ <*S*>)) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(1 + 1) + (len a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

(<*A*> ^ (a ^ <*S*>)) . 2 is set
2 - () is V28() V186() ext-real set
(a ^ <*S*>) . (2 - ()) is set
2 - 1 is V28() V186() ext-real set
(a ^ <*S*>) . (2 - 1) is set
a . 1 is set
L . 1 is set
L . (1 + 1) is set
(L . 1) /\ (L . (1 + 1)) is set

dom L2 is set
L2 is Element of bool the carrier of I
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L2 is Element of bool the carrier of I
L1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

dom L3 is set
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

dom L2 is set
L1 - 1 is V28() V186() ext-real set
dom (<*A*> ^ a) is countable Element of bool NAT
(<*A*> ^ a) . L1 is set
L2 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
a . L2 is set
L2 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . L1 is set
L1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(<*A*> ^ a) . (L1 + 1) is set
(L1 + 1) - () is V28() V186() ext-real set
a . ((L1 + 1) - ()) is set

dom x is set
a . L1 is set
L . L1 is set

dom x is set
L . (L1 + 1) is set
(L . L1) /\ (L . (L1 + 1)) is set
L3 is Element of bool the carrier of I

dom x is set
L . L2 is set

dom x is set
L . L2 is set
L . (L2 + 1) is set
(L . L2) /\ (L . (L2 + 1)) is set
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
0 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L2 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
L2 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT

dom L2 is set
1 + (len a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
dom (<*A*> ^ a) is countable Element of bool NAT
(<*A*> ^ a) . L1 is set
((len a) + 1) - 1 is V28() V186() ext-real set
a . (((len a) + 1) - 1) is set
a . (len a) is set
L . (len a) is set

dom L2 is set
L . (len a) is set
L . ((len a) + 1) is set
(L . (len a)) /\ (L . ((len a) + 1)) is set
L2 is Element of bool the carrier of I

dom L3 is set
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty () () () () TopStruct

(I,A) is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),(I,A) #) is strict TopStruct
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
S is Element of bool the carrier of (I,A)
card S is V21() V22() V23() cardinal set
B is set
l is set
L is Element of the carrier of (I,A)
a is Element of the carrier of (I,A)
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
bool (bool the carrier of (I,A)) is non empty set
{L,a} is non empty finite countable Element of bool the carrier of (I,A)
b is Element of the topology of (I,A)

card () is V21() V22() V23() cardinal set
a1 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
dom a1 is set

dom b1 is set

dom a is set
(I,a1) is Element of I
b1 . (I,a1) is set
a . (I,a1) is set
C is set
b1 . C is set
a . C is set

Li is Element of I
C . Li is set
a1 . Li is set

a . Li is set
j is Element of the carrier of (I,A)
{j,a} is non empty finite countable Element of bool the carrier of (I,A)
o is Element of the topology of (I,A)
L1 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A

(I,L1) is Element of I
L1 . (I,L1) is set
(I,A,(I,L1)) is non empty () () () () TopStruct
the topology of (I,A,(I,L1)) is non empty Element of bool (bool the carrier of (I,A,(I,L1)))
the carrier of (I,A,(I,L1)) is non empty set
bool the carrier of (I,A,(I,L1)) is non empty set
bool (bool the carrier of (I,A,(I,L1))) is non empty set
L1 . (I,a1) is set
L2 is set
{L2} is non empty trivial finite 1 -element countable set
dom L1 is set
b1 . Li is set
{j,L} is non empty finite countable Element of bool the carrier of (I,A)
L3 is Element of the topology of (I,A)

(I,x) is Element of I
x . (I,x) is set
(I,A,(I,x)) is non empty () () () () TopStruct
the topology of (I,A,(I,x)) is non empty Element of bool (bool the carrier of (I,A,(I,x)))
the carrier of (I,A,(I,x)) is non empty set
bool the carrier of (I,A,(I,x)) is non empty set
bool (bool the carrier of (I,A,(I,x))) is non empty set
x . (I,a1) is set
y is set
{y} is non empty trivial finite 1 -element countable set
dom x is set
C . (I,a1) is set
pi (S,(I,a1)) is set
card (pi (S,(I,a1))) is V21() V22() V23() cardinal set
C is non empty non trivial set
a1 +* ((I,a1),C) is Relation-like I -defined Function-like V14(I) set
j is set
(a1 +* ((I,a1),C)) . j is set
() . j is set
a1 . j is set
Li is set
dom () is set

o . j is set

(I,j) is Element of I
(I,A,(I,j)) is non empty () () () () TopStruct
the carrier of (I,A,(I,j)) is non empty set
bool the carrier of (I,A,(I,j)) is non empty set
j . (I,j) is set
dom j is set
j . (I,a1) is set
Li is set
L1 is set
L2 is Element of I

o . L1 is set
j . L1 is set
L2 is Element of I

o . L2 is set
a1 . L2 is set
o . L1 is set
j . L1 is set
L2 is Element of I

dom o is set
Li is set

dom o is set
o . (I,a1) is set

L1 . (I,a1) is set
L3 is set
o . L3 is set

L2 . L3 is set
x is Element of I
a1 . x is set
a1 . L3 is set
y is set
{y} is non empty trivial finite 1 -element countable set

L2 . x is set
o . x is set
j . x is set
o . L3 is set
L2 . L3 is set

dom L2 is set
Li is Element of bool the carrier of (I,A,(I,j))
o is Element of the carrier of (I,A,(I,j))
L1 is Element of the carrier of (I,A,(I,j))
b1 +* ((I,j),L1) is Relation-like I -defined Function-like V14(I) set
b1 +* ((I,j),o) is Relation-like I -defined Function-like V14(I) set
L3 is Element of the carrier of (I,A)
L2 is Element of the carrier of (I,A)

x . (I,j) is set
y1 is set
x . y1 is set
j . y1 is set
b1 . y1 is set

y1 is set
y . y1 is set
j . y1 is set
b1 . y1 is set
dom y is set
dom x is set
{L3,L2} is non empty finite countable Element of bool the carrier of (I,A)
y1 is Element of the topology of (I,A)
y . (I,j) is set
x1 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A

(I,x1) is Element of I
x1 . (I,x1) is set
(I,A,(I,x1)) is non empty () () () () TopStruct
the topology of (I,A,(I,x1)) is non empty Element of bool (bool the carrier of (I,A,(I,x1)))
the carrier of (I,A,(I,x1)) is non empty set
bool the carrier of (I,A,(I,x1)) is non empty set
bool (bool the carrier of (I,A,(I,x1))) is non empty set
dom x1 is set
x1 . (I,j) is set
card (x1 . (I,j)) is V21() V22() V23() cardinal set
the topology of (I,A,(I,j)) is non empty Element of bool (bool the carrier of (I,A,(I,j)))
bool (bool the carrier of (I,A,(I,j))) is non empty set
{o,L1} is non empty finite countable Element of bool the carrier of (I,A,(I,j))
e is Element of the topology of (I,A,(I,j))
the topology of (I,A,(I,j)) is non empty Element of bool (bool the carrier of (I,A,(I,j)))
bool (bool the carrier of (I,A,(I,j))) is non empty set
o is Element of the topology of (I,A,(I,j))
o /\ Li is Element of bool the carrier of (I,A,(I,j))
card (o /\ Li) is V21() V22() V23() cardinal set
card o is V21() V22() V23() cardinal set
L1 is non empty non trivial set
j +* ((I,j),L1) is Relation-like I -defined Function-like V14(I) set
L2 is set
(j +* ((I,j),L1)) . L2 is set
() . L2 is set
j . L2 is set
L2 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
L2 . (I,j) is set
(I,L2) is Element of I
L2 . (I,L2) is set
(I,A,(I,L2)) is non empty () () () () TopStruct
the topology of (I,A,(I,L2)) is non empty Element of bool (bool the carrier of (I,A,(I,L2)))
the carrier of (I,A,(I,L2)) is non empty set
bool the carrier of (I,A,(I,L2)) is non empty set
bool (bool the carrier of (I,A,(I,L2))) is non empty set

x is set
y is set
b1 +* ((I,j),y) is Relation-like I -defined Function-like V14(I) set
dom (b1 +* ((I,j),y)) is set
x1 is set
(b1 +* ((I,j),y)) . x1 is set
b1 . x1 is set
j . x1 is set
(b1 +* ((I,j),y)) . x1 is set
j . x1 is set
dom L2 is set
x1 is set
(b1 +* ((I,j),y)) . x1 is set
b1 . x1 is set
j . x1 is set
L2 . x1 is set
(b1 +* ((I,j),y)) . x1 is set
L2 . x1 is set
L3 is Element of the topology of (I,A)
L3 /\ S is Element of bool the carrier of (I,A)
b1 +* ((I,j),x) is Relation-like I -defined Function-like V14(I) set
dom (b1 +* ((I,j),x)) is set
e is set
(b1 +* ((I,j),x)) . e is set
b1 . e is set
j . e is set
(b1 +* ((I,j),x)) . e is set
j . e is set
(b1 +* ((I,j),x)) . (I,j) is set
(b1 +* ((I,j),y)) . (I,j) is set
e is set
(b1 +* ((I,j),x)) . e is set
b1 . e is set
j . e is set
L2 . e is set
(b1 +* ((I,j),x)) . e is set
L2 . e is set
card (L3 /\ S) is V21() V22() V23() cardinal set
e is set
f is set

dom o is set
o is set

f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
(f +* ((I,j),e)) . o is set
f . o is set
L2 . o is set

dom c28 is set

f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
(f +* ((I,j),e)) . o is set

dom c28 is set
L2 . o is set

f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set

f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
dom (f +* ((I,j),e)) is set
(f +* ((I,j),e)) . (I,j) is set

dom o is set

(I,B) is Element of I
(I,A,(I,B)) is non empty () () () () TopStruct
the carrier of (I,A,(I,B)) is non empty set
bool the carrier of (I,A,(I,B)) is non empty set
B . (I,B) is set
dom B is set
dom () is set
l is Element of the carrier of (I,A)
L is Element of the carrier of (I,A)

dom a is set

dom L is set

a1 . (I,B) is set

b . (I,B) is set
b1 is set
a1 . b1 is set
b . b1 is set
a1 . b1 is set
b . b1 is set
() . (I,B) is set
b1 is Element of bool the carrier of (I,A,(I,B))
a is Element of the carrier of (I,A,(I,B))
C is Element of the carrier of (I,A,(I,B))
the topology of (I,A,(I,B)) is non empty Element of bool (bool the carrier of (I,A,(I,B)))
bool (bool the carrier of (I,A,(I,B))) is non empty set
{C,a} is non empty finite countable Element of bool the carrier of (I,A,(I,B))
j is Element of the topology of (I,A,(I,B))

dom {a1} is set
{a1} +* ((I,B),j) is Relation-like I -defined Function-like V14(I) set
dom ({a1} +* ((I,B),j)) is set
Li is set
b . Li is set
({a1} +* ((I,B),j)) . Li is set
a1 . Li is set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
{a1} . Li is finite countable set
Li is set
({a1} +* ((I,B),j)) . Li is set
() . Li is set
a1 . Li is set
o is Element of I
() . o is set
(I,A,o) is non empty () () () () TopStruct
the carrier of (I,A,o) is non empty set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
{a1} . Li is finite countable set
Li is Element of I
({a1} +* ((I,B),j)) . Li is set
{a1} . Li is finite countable set
a1 . Li is set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
Li is set
a1 . Li is set
({a1} +* ((I,B),j)) . Li is set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
{a1} . Li is finite countable set
({a1} +* ((I,B),j)) . (I,B) is set
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
bool (bool the carrier of (I,A)) is non empty set
product ({a1} +* ((I,B),j)) is functional with_common_domain product-like set
dom b is set
Li is Element of the topology of (I,A)
dom a1 is set
{l,L} is non empty finite countable Element of bool the carrier of (I,A)
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
bool (bool the carrier of (I,A)) is non empty set
l is Element of the topology of (I,A)
l /\ S is Element of bool the carrier of (I,A)
card (l /\ S) is V21() V22() V23() cardinal set

a is set
b is set
card l is V21() V22() V23() cardinal set

dom L is set
(I,L) is Element of I
a is set
L . a is set
B . a is set
() . (I,B) is set
j is Element of I
L . j is set
(I,A,j) is non empty () () () () TopStruct
the topology of (I,A,j) is non empty Element of bool (bool the carrier of (I,A,j))
the carrier of (I,A,j) is non empty set