:: MATROID0 semantic presentation

REAL is V221() V222() V223() V227() set
NAT is non empty non trivial V31() non finite cardinal limit_cardinal non empty-membered V221() V222() V223() V224() V225() V226() V227() Element of K19(REAL)
K19(REAL) is non empty set
NAT is non empty non trivial V31() non finite cardinal limit_cardinal non empty-membered V221() V222() V223() V224() V225() V226() V227() set
K19(NAT) is non empty non trivial non finite non empty-membered set
K19(NAT) is non empty non trivial non finite non empty-membered set
0 is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() V227() Element of NAT
{} is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() set
the empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() set is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() set
1 is non empty V31() V35() finite cardinal V121() ext-real positive V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
2 is non empty V31() V35() finite cardinal V121() ext-real positive V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
K260(0,1,2) is non empty finite V221() V222() V223() V224() V225() V226() set
K20(K260(0,1,2),K260(0,1,2)) is non empty finite set
K20(K20(K260(0,1,2),K260(0,1,2)),K260(0,1,2)) is non empty finite set
K19(K20(K20(K260(0,1,2),K260(0,1,2)),K260(0,1,2))) is non empty finite finite-membered set
K19(K20(K260(0,1,2),K260(0,1,2))) is non empty finite finite-membered set
COMPLEX is V221() V227() set
RAT is V221() V222() V223() V224() V227() set
INT is V221() V222() V223() V224() V225() V227() set
K501() is set
{{}} is non empty trivial finite finite-membered 1 -element V221() V222() V223() V224() V225() V226() set
K288({{}}) is M23({{}})
K20(K288({{}}),{{}}) is set
K19(K20(K288({{}}),{{}})) is non empty set
K36(K288({{}}),{{}}) is set
union {} is finite set
M is TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
M is TopStruct
the topology of M is Element of K19(K19( the carrier of M))
the carrier of M is set
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
M is TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M) is Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is Element of K19(K19( the carrier of M))
K19({{}}) is non empty finite finite-membered set
K19(K19({{}})) is non empty finite finite-membered set
bool {{}} is non empty finite finite-membered Element of K19(K19({{}}))
M is finite finite-membered Element of K19(K19({{}}))
TopStruct(# {{}},M #) is strict TopStruct
A is strict TopStruct
the carrier of A is set
the topology of A is Element of K19(K19( the carrier of A))
K19( the carrier of A) is non empty set
K19(K19( the carrier of A)) is non empty set
(A) is Element of K19(K19( the carrier of A))
B is finite Element of K19( the carrier of A)
C is finite Element of K19( the carrier of A)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card B) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
C \ B is finite Element of K19( the carrier of A)
e is Element of the carrier of A
{e} is non empty trivial finite 1 -element set
B \/ {e} is non empty finite set
{{},{{}}} is non empty finite finite-membered set
M is non void TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the Element of the topology of M is Element of the topology of M
B is Element of K19( the carrier of M)
(M) is Element of K19(K19( the carrier of M))
M is () TopStruct
(M) is Element of K19(K19( the carrier of M))
the carrier of M is set
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
the topology of M is Element of K19(K19( the carrier of M))
M is non void () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is open Element of K19( the carrier of M)
B is set
(M) is subset-closed Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
M is non void () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the Element of the topology of M is Element of the topology of M
B is open Element of K19( the carrier of M)
C is open Element of K19( the carrier of M)
M is () TopStruct
(M) is subset-closed Element of K19(K19( the carrier of M))
the carrier of M is set
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
the topology of M is Element of K19(K19( the carrier of M))
A is non void () TopStruct
the carrier of A is set
K19( the carrier of A) is non empty set
the open Element of K19( the carrier of A) is open Element of K19( the carrier of A)
M is non void () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M) is subset-closed Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
M is non void TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of K19( the carrier of M)
A is set
(M) is Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
B is set
M is non void () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is open Element of K19( the carrier of M)
B is set
A /\ B is Element of K19( the carrier of M)
C is Element of K19( the carrier of M)
B /\ A is open Element of K19( the carrier of M)
C is Element of K19( the carrier of M)
A \ B is Element of K19( the carrier of M)
C is Element of K19( the carrier of M)
M is non empty non void TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
(M) is Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
A is finite Element of K19( the carrier of M)
B is finite Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B \ A is finite Element of K19( the carrier of M)
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {C} is non empty finite Element of K19( the carrier of M)
A is finite Element of K19( the carrier of M)
(M) is Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
B is finite Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B \ A is finite Element of K19( the carrier of M)
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {C} is non empty finite Element of K19( the carrier of M)
{C} is non empty trivial finite 1 -element set
A \/ {C} is non empty finite set
M is TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is V31() V35() finite cardinal V121() ext-real V125() set
M is TopStruct
the carrier of M is set
B is set
(M) is Element of K19(K19( the carrier of M))
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
the topology of M is Element of K19(K19( the carrier of M))
A is finite set
K19( the carrier of M) is non empty set
A is finite set
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B is finite Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
{{{}}} is non empty trivial finite finite-membered 1 -element with_non-empty_elements non empty-membered set
A is finite set
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is finite set
card M is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
A \ M is finite Element of K19(A)
K19(A) is non empty finite finite-membered set
B is set
M is non empty mutually-disjoint with_non-empty_elements non empty-membered set
union M is non empty set
A is V1() V4(M) V5( union M) Function-like V18(M, union M) Choice_Function of M
B is set
K48(A) is set
C is set
A . B is set
A . C is set
dom A is Element of K19(M)
K19(M) is non empty set
M is TopSpace-like discrete V102() TopStruct
the topology of M is Element of K19(K19( the carrier of M))
the carrier of M is set
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
A is Element of K19( the carrier of M)
B is Element of K19( the carrier of M)
A is finite Element of K19( the carrier of M)
(M) is Element of K19(K19( the carrier of M))
B is finite Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B \ A is finite Element of K19( the carrier of M)
(card B) + {} is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
C is set
e is Element of the carrier of M
{e} is non empty trivial finite 1 -element set
A \/ {e} is non empty finite set
c is Element of K19( the carrier of M)
M is non empty TopSpace-like discrete V102() V103() V104() non void () () TopStruct
M is set
union M is set
K19((union M)) is non empty set
{ b₁ where b₁ is Element of K19((union M)) : for b₂ being set holds
( not b₂ in M or ex b₃ being set st b₁ /\ b₂ c= {b₃} ) } is set
bool (union M) is non empty Element of K19(K19((union M)))
K19(K19((union M))) is non empty set
C is set
e is Element of K19((union M))
C is Element of K19(K19((union M)))
TopStruct(# (union M),C #) is strict TopStruct
the carrier of TopStruct(# (union M),C #) is set
(TopStruct(# (union M),C #)) is Element of K19(K19( the carrier of TopStruct(# (union M),C #)))
K19( the carrier of TopStruct(# (union M),C #)) is non empty set
K19(K19( the carrier of TopStruct(# (union M),C #))) is non empty set
the topology of TopStruct(# (union M),C #) is Element of K19(K19( the carrier of TopStruct(# (union M),C #)))
A is strict TopStruct
the carrier of A is set
(A) is Element of K19(K19( the carrier of A))
K19( the carrier of A) is non empty set
K19(K19( the carrier of A)) is non empty set
the topology of A is Element of K19(K19( the carrier of A))
B is strict TopStruct
the carrier of B is set
(B) is Element of K19(K19( the carrier of B))
K19( the carrier of B) is non empty set
K19(K19( the carrier of B)) is non empty set
the topology of B is Element of K19(K19( the carrier of B))
M is non empty with_non-empty_elements non empty-membered set
(M) is strict TopStruct
the carrier of (M) is set
union M is non empty set
M is set
(M) is strict TopStruct
the carrier of (M) is set
K19( the carrier of (M)) is non empty set
((M)) is Element of K19(K19( the carrier of (M)))
K19(K19( the carrier of (M))) is non empty set
the topology of (M) is Element of K19(K19( the carrier of (M)))
union M is set
K19((union M)) is non empty set
{ b₁ where b₁ is Element of K19((union M)) : for b₂ being set holds
( not b₂ in M or ex b₃ being set st b₁ /\ b₂ c= {b₃} ) } is set
B is Element of K19( the carrier of (M))
C is Element of M
B /\ C is Element of K19( the carrier of (M))
{} /\ C is finite V221() V222() V223() V224() V225() V226() set
{1} is non empty trivial finite finite-membered 1 -element with_non-empty_elements non empty-membered V221() V222() V223() V224() V225() V226() Element of K19(NAT)
e is Element of K19((union M))
e is set
{e} is non empty trivial finite 1 -element set
the Element of C is Element of C
{ the Element of C} is non empty trivial finite 1 -element set
C is set
B /\ C is Element of K19( the carrier of (M))
e is Element of C
{e} is non empty trivial finite 1 -element set
M is set
(M) is strict TopStruct
((M)) is Element of K19(K19( the carrier of (M)))
the carrier of (M) is set
K19( the carrier of (M)) is non empty set
K19(K19( the carrier of (M))) is non empty set
the topology of (M) is Element of K19(K19( the carrier of (M)))
union M is set
K19((union M)) is non empty set
{ b₁ where b₁ is Element of K19((union M)) : for b₂ being set holds
( not b₂ in M or ex b₃ being set st b₁ /\ b₂ c= {b₃} ) } is set
{} (union M) is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() Element of K19((union M))
C is set
({} (union M)) /\ C is finite V221() V222() V223() V224() V225() V226() Element of K19((union M))
e is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() set
{e} is non empty trivial finite finite-membered 1 -element V221() V222() V223() V224() V225() V226() set
C is set
e is set
c is set
C /\ c is set
b is Element of K19((union M))
b is set
{b} is non empty trivial finite 1 -element set
e /\ c is set
D is set
{D} is non empty trivial finite 1 -element set
c is Element of K19((union M))
M is mutually-disjoint set
(M) is strict non void () TopStruct
the carrier of (M) is set
K19( the carrier of (M)) is non empty set
A is Element of K19( the carrier of (M))
K20(A,M) is set
K19(K20(A,M)) is non empty set
B is set
union M is set
C is set
B is V1() V4(A) V5(M) Function-like V18(A,M) Element of K19(K20(A,M))
C is set
B . C is set
M is mutually-disjoint set
(M) is strict non void () TopStruct
the carrier of (M) is set
K19( the carrier of (M)) is non empty set
A is Element of K19( the carrier of (M))
K20(A,M) is set
K19(K20(A,M)) is non empty set
B is V1() V4(A) V5(M) Function-like V18(A,M) Element of K19(K20(A,M))
C is set
K48(B) is set
e is set
B . C is set
B . e is set
dom B is Element of K19(A)
K19(A) is non empty set
rng B is Element of K19(M)
K19(M) is non empty set
c is Element of M
A /\ c is Element of K19( the carrier of (M))
b is Element of M
A /\ b is Element of K19( the carrier of (M))
D is Element of b
{D} is non empty trivial finite 1 -element set
C is Element of M
the Element of C is Element of C
A /\ C is Element of K19( the carrier of (M))
{ the Element of C} is non empty trivial finite 1 -element set
c is set
B . c is set
union M is set
dom B is Element of K19(A)
K19(A) is non empty set
b is set
rng B is Element of K19(M)
K19(M) is non empty set
{c} is non empty trivial finite 1 -element set
b is set
B . b is set
M is mutually-disjoint set
(M) is strict non void () TopStruct
((M)) is subset-closed Element of K19(K19( the carrier of (M)))
the carrier of (M) is set
K19( the carrier of (M)) is non empty set
K19(K19( the carrier of (M))) is non empty set
the topology of (M) is non empty Element of K19(K19( the carrier of (M)))
union M is set
K19((union M)) is non empty set
{ b₁ where b₁ is Element of K19((union M)) : for b₂ being set holds
( not b₂ in M or ex b₃ being set st b₁ /\ b₂ c= {b₃} ) } is set
B is finite Element of K19( the carrier of (M))
C is finite Element of K19( the carrier of (M))
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card B) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
C \ B is finite Element of K19( the carrier of (M))
K20(B,M) is set
K19(K20(B,M)) is non empty set
e is V1() V4(B) V5(M) Function-like V18(B,M) finite Element of K19(K20(B,M))
K20(C,M) is set
K19(K20(C,M)) is non empty set
c is V1() V4(C) V5(M) Function-like V18(C,M) finite Element of K19(K20(C,M))
dom e is finite Element of K19(B)
K19(B) is non empty finite finite-membered set
rng e is finite Element of K19(M)
K19(M) is non empty set
rng c is finite Element of K19(M)
b is finite set
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
dom c is finite Element of K19(C)
K19(C) is non empty finite finite-membered set
D is finite set
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D \ b is finite Element of K19(D)
K19(D) is non empty finite finite-membered set
x is set
Ae is set
c . Ae is set
Be is Element of the carrier of (M)
{Be} is non empty trivial finite 1 -element set
B \/ {Be} is non empty finite set
c . Be is set
e . Be is set
D is Element of K19( the carrier of (M))
B \/ D is Element of K19( the carrier of (M))
c is Element of K19((union M))
e is set
c /\ e is Element of K19((union M))
B /\ e is finite Element of K19( the carrier of (M))
D /\ e is Element of K19( the carrier of (M))
(B /\ e) \/ (D /\ e) is Element of K19( the carrier of (M))
x is Element of e
{x} is non empty trivial finite 1 -element set
a is set
e . a is set
e is set
{e} is non empty trivial finite 1 -element set
e is set
a is set
{a} is non empty trivial finite 1 -element set
M is finite set
bool M is non empty finite finite-membered Element of K19(K19(M))
K19(M) is non empty finite finite-membered set
K19(K19(M)) is non empty finite finite-membered set
K19((bool M)) is non empty finite finite-membered set
A is finite finite-membered Element of K19((bool M))
(A) is strict non void () TopStruct
union A is finite Element of K19(M)
the carrier of (A) is set
M is set
A is with_non-empty_elements a_partition of M
B is set
C is set
the non empty finite set is non empty finite set
the non empty finite finite-membered mutually-disjoint with_non-empty_elements non empty-membered a_partition of the non empty finite set is non empty finite finite-membered mutually-disjoint with_non-empty_elements non empty-membered a_partition of the non empty finite set
( the non empty finite finite-membered mutually-disjoint with_non-empty_elements non empty-membered a_partition of the non empty finite set ) is non empty finite strict non void () () () () TopStruct
M is non void () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is open Element of K19( the carrier of M)
(M) is Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) VectSpStr over M
the carrier of A is non empty set
K19( the carrier of A) is non empty set
{ b₁ where b₁ is Element of K19( the carrier of A) : b₁ is linearly-independent } is set
bool the carrier of A is non empty Element of K19(K19( the carrier of A))
K19(K19( the carrier of A)) is non empty set
e is set
c is Element of K19( the carrier of A)
e is Element of K19(K19( the carrier of A))
TopStruct(# the carrier of A,e #) is strict TopStruct
the carrier of TopStruct(# the carrier of A,e #) is set
(TopStruct(# the carrier of A,e #)) is Element of K19(K19( the carrier of TopStruct(# the carrier of A,e #)))
K19( the carrier of TopStruct(# the carrier of A,e #)) is non empty set
K19(K19( the carrier of TopStruct(# the carrier of A,e #))) is non empty set
the topology of TopStruct(# the carrier of A,e #) is Element of K19(K19( the carrier of TopStruct(# the carrier of A,e #)))
B is strict TopStruct
the carrier of B is set
(B) is Element of K19(K19( the carrier of B))
K19( the carrier of B) is non empty set
K19(K19( the carrier of B)) is non empty set
the topology of B is Element of K19(K19( the carrier of B))
C is strict TopStruct
the carrier of C is set
(C) is Element of K19(K19( the carrier of C))
K19( the carrier of C) is non empty set
K19(K19( the carrier of C)) is non empty set
the topology of C is Element of K19(K19( the carrier of C))
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) VectSpStr over M
(M,A) is strict TopStruct
((M,A)) is Element of K19(K19( the carrier of (M,A)))
the carrier of (M,A) is set
K19( the carrier of (M,A)) is non empty set
K19(K19( the carrier of (M,A))) is non empty set
the topology of (M,A) is Element of K19(K19( the carrier of (M,A)))
the carrier of A is non empty set
K19( the carrier of A) is non empty set
{ b₁ where b₁ is Element of K19( the carrier of A) : b₁ is linearly-independent } is set
{} A is empty proper V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() linearly-independent Element of K19( the carrier of A)
C is set
e is set
b is Element of K19( the carrier of A)
c is Element of K19( the carrier of A)
b is Element of K19( the carrier of A)
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) VectSpStr over M
(M,A) is non empty strict non void () TopStruct
the carrier of (M,A) is non empty set
K19( the carrier of (M,A)) is non empty set
the carrier of A is non empty set
K19( the carrier of A) is non empty set
C is Element of K19( the carrier of (M,A))
((M,A)) is subset-closed Element of K19(K19( the carrier of (M,A)))
K19(K19( the carrier of (M,A))) is non empty set
the topology of (M,A) is non empty Element of K19(K19( the carrier of (M,A)))
{ b₁ where b₁ is Element of K19( the carrier of A) : b₁ is linearly-independent } is set
e is Element of K19( the carrier of A)
e is Element of K19( the carrier of A)
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) VectSpStr over M
the carrier of A is non empty set
K19( the carrier of A) is non empty set
C is finite Element of K19( the carrier of A)
B is finite Element of K19( the carrier of A)
Lin B is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() strict V185(M) V186(M) V187(M) V188(M) M20(M,A)
Lin C is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() strict V185(M) V186(M) V187(M) V188(M) M20(M,A)
B \ C is finite Element of K19( the carrier of A)
C \/ (B \ C) is finite Element of K19( the carrier of A)
e is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
{e} is non empty trivial finite 1 -element Element of K19( the carrier of A)
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) VectSpStr over M
the carrier of A is non empty set
K19( the carrier of A) is non empty set
B is Element of K19( the carrier of A)
Lin B is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() strict V185(M) V186(M) V187(M) V188(M) M20(M,A)
the carrier of (Lin B) is non empty set
the carrier of M is non empty non trivial non empty-membered set
{ (Sum b₁) where b₁ is V1() V4( the carrier of A) V5( the carrier of M) Function-like V18( the carrier of A, the carrier of M) Linear_Combination of B : verum } is set
C is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
{C} is non empty trivial finite 1 -element Element of K19( the carrier of A)
B \/ {C} is non empty Element of K19( the carrier of A)
0. A is V57(A) V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
the ZeroF of A is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
c is V1() V4( the carrier of A) V5( the carrier of M) Function-like V18( the carrier of A, the carrier of M) Linear_Combination of B \/ {C}
Sum c is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
Carrier c is finite Element of K19( the carrier of A)
c ! {C} is V1() V4( the carrier of A) V5( the carrier of M) Function-like V18( the carrier of A, the carrier of M) Linear_Combination of {C}
(c ! {C}) . C is V127(M) V128(M) V129(M) V134(M) V135(M) V136(M) Element of the carrier of M
c . C is V127(M) V128(M) V129(M) V134(M) V135(M) V136(M) Element of the carrier of M
b is set
D is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
(B \/ {C}) \ B is Element of K19( the carrier of A)
c ! B is V1() V4( the carrier of A) V5( the carrier of M) Function-like V18( the carrier of A, the carrier of M) Linear_Combination of B
(c ! B) + (c ! {C}) is V1() V4( the carrier of A) V5( the carrier of M) Function-like V18( the carrier of A, the carrier of M) Linear_Combination of A
Sum (c ! B) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
Sum (c ! {C}) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
(Sum (c ! B)) + (Sum (c ! {C})) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
(c . C) * C is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
(Sum (c ! B)) + ((c . C) * C) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
- (Sum (c ! B)) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
(c . C) " is V127(M) V128(M) V129(M) V134(M) V135(M) V136(M) Element of the carrier of M
- ((c . C) ") is V127(M) V128(M) V129(M) V134(M) V135(M) V136(M) Element of the carrier of M
(- ((c . C) ")) * (c ! B) is V1() V4( the carrier of A) V5( the carrier of M) Function-like V18( the carrier of A, the carrier of M) Linear_Combination of A
0. M is V57(M) V127(M) V128(M) V129(M) V134(M) V135(M) V136(M) Element of the carrier of M
the ZeroF of M is V127(M) V128(M) V129(M) V134(M) V135(M) V136(M) Element of the carrier of M
((c . C) ") * (- (Sum (c ! B))) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
((c . C) ") * (Sum (c ! B)) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
- (((c . C) ") * (Sum (c ! B))) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
(- ((c . C) ")) * (Sum (c ! B)) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
Sum ((- ((c . C) ")) * (c ! B)) is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
b is set
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) VectSpStr over M
(M,A) is non empty strict non void () TopStruct
((M,A)) is subset-closed Element of K19(K19( the carrier of (M,A)))
the carrier of (M,A) is non empty set
K19( the carrier of (M,A)) is non empty set
K19(K19( the carrier of (M,A))) is non empty set
the topology of (M,A) is non empty Element of K19(K19( the carrier of (M,A)))
the carrier of A is non empty set
K19( the carrier of A) is non empty set
{ b₁ where b₁ is Element of K19( the carrier of A) : b₁ is linearly-independent } is set
C is finite Element of K19( the carrier of (M,A))
e is finite Element of K19( the carrier of (M,A))
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card C) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e \ C is finite Element of K19( the carrier of (M,A))
c is finite linearly-independent Element of K19( the carrier of A)
b is finite linearly-independent Element of K19( the carrier of A)
c \/ b is finite Element of K19( the carrier of A)
Lin (c \/ b) is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() strict V185(M) V186(M) V187(M) V188(M) M20(M,A)
the carrier of (Lin (c \/ b)) is non empty set
x is set
K19( the carrier of (Lin (c \/ b))) is non empty set
Ae is set
x is finite linearly-independent Element of K19( the carrier of (Lin (c \/ b)))
Ae is finite linearly-independent Element of K19( the carrier of (Lin (c \/ b)))
x \/ Ae is finite Element of K19( the carrier of (Lin (c \/ b)))
Lin (x \/ Ae) is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() strict V185(M) V186(M) V187(M) V188(M) M20(M, Lin (c \/ b))
Be is Basis of Lin (c \/ b)
D is Basis of Lin (c \/ b)
c is finite set
card c is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card Be is V31() cardinal set
Lin c is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() strict V185(M) V186(M) V187(M) V188(M) M20(M,A)
the carrier of (Lin c) is non empty set
D \ the carrier of (Lin c) is Element of K19( the carrier of (Lin (c \/ b)))
the Element of D \ the carrier of (Lin c) is Element of D \ the carrier of (Lin c)
K19( the carrier of (Lin c)) is non empty set
x is Element of K19( the carrier of (Lin c))
e is Element of K19( the carrier of A)
a is Basis of Lin c
card a is V31() cardinal set
x is set
C \/ e is finite Element of K19( the carrier of (M,A))
e is Element of the carrier of (M,A)
{e} is non empty trivial finite 1 -element set
C \/ {e} is non empty finite set
a is set
a is V127(A) V128(A) V129(A) V134(A) V135(A) V136(A) Element of the carrier of A
{a} is non empty trivial finite 1 -element Element of K19( the carrier of A)
c \/ {a} is non empty finite Element of K19( the carrier of A)
{e} is non empty trivial finite 1 -element Element of K19( the carrier of (M,A))
C \/ {e} is non empty finite Element of K19( the carrier of (M,A))
M is non empty non degenerated non trivial V130() V131() V132() V137() V138() V139() V158() V163() V164() V165() V170() V172() V174() V176() right-distributive left-distributive right_unital well-unital V182() left_unital L15()
A is non empty V130() V131() V132() V137() V138() V139() V163() V164() V165() V170() V185(M) V186(M) V187(M) V188(M) finite-dimensional VectSpStr over M
(M,A) is non empty strict non void () () TopStruct
B is set
((M,A)) is subset-closed Element of K19(K19( the carrier of (M,A)))
the carrier of (M,A) is non empty set
K19( the carrier of (M,A)) is non empty set
K19(K19( the carrier of (M,A))) is non empty set
the topology of (M,A) is non empty Element of K19(K19( the carrier of (M,A)))
the carrier of A is non empty set
K19( the carrier of A) is non empty set
M is TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
M is non void () () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
B is Element of K19( the carrier of M)
A is Element of K19( the carrier of M)
e is V31() V35() finite cardinal V121() ext-real V125() set
c is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is finite Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is V31() V35() finite cardinal V121() ext-real V125() set
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
{} + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card C) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D is V31() V35() finite cardinal V121() ext-real V125() set
1 + D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
x is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
Ae is finite Element of K19( the carrier of M)
card Ae is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
x + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
x + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D is finite open Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D is finite open Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
x is Element of K19( the carrier of M)
Ae is finite open Element of K19( the carrier of M)
card Ae is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non void () () () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
{} M is empty V31() V35() finite finite-membered cardinal {} -element open V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() Element of K19( the carrier of M)
B is finite open Element of K19( the carrier of M)
M is non empty non void () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
B is finite open Element of K19( the carrier of M)
A is Element of K19( the carrier of M)
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card B) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e is set
card e is V31() cardinal set
c is finite Element of K19( the carrier of M)
c \ B is finite Element of K19( the carrier of M)
b is Element of the carrier of M
{b} is non empty trivial finite 1 -element Element of K19( the carrier of M)
B \/ {b} is non empty finite Element of K19( the carrier of M)
B is finite open Element of K19( the carrier of M)
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
A is finite Element of K19( the carrier of M)
(M) is subset-closed Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
B is finite Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B \ A is finite Element of K19( the carrier of M)
A \/ B is finite Element of K19( the carrier of M)
C is Element of K19( the carrier of M)
e is finite open Element of K19( the carrier of M)
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
c is finite open Element of K19( the carrier of M)
b is Element of K19( the carrier of M)
D is set
x is Element of the carrier of M
B \ c is finite Element of K19( the carrier of M)
{x} is non empty trivial finite 1 -element Element of K19( the carrier of M)
c \/ {x} is non empty finite Element of K19( the carrier of M)
card c is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
C is V31() V35() finite cardinal V121() ext-real V125() set
e is finite open Element of K19( the carrier of M)
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e is V31() V35() finite cardinal V121() ext-real V125() set
c is set
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
{} M is empty proper V31() V35() finite finite-membered cardinal {} -element open V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() Element of K19( the carrier of M)
b is finite open Element of K19( the carrier of M)
c is V31() V35() finite cardinal V121() ext-real V125() set
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card {} is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() V227() Element of NAT
c is V31() V35() finite cardinal V121() ext-real V125() set
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D is finite open Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is finite open Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
{} M is empty proper V31() V35() finite finite-membered cardinal {} -element open V121() ext-real V125() V221() V222() V223() V224() V225() V226() V227() Element of K19( the carrier of M)
card {} is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() V227() Element of NAT
C is V31() V35() finite cardinal V121() ext-real V125() set
e is finite open Element of K19( the carrier of M)
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e is V31() V35() finite cardinal V121() ext-real V125() set
c is set
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is finite open Element of K19( the carrier of M)
c is V31() V35() finite cardinal V121() ext-real V125() set
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
c is V31() V35() finite cardinal V121() ext-real V125() set
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D is finite open Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
D is finite open Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e is finite open Element of K19( the carrier of M)
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
c is finite open Element of K19( the carrier of M)
card c is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b is Element of K19( the carrier of M)
D is finite open Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is finite Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B is finite open Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is finite Element of K19( the carrier of M)
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
[#] M is non empty non proper Element of K19( the carrier of M)
the carrier of M is non empty set
K19( the carrier of M) is non empty set
(M,([#] M)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= [#] M } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= [#] M } is set
M is non void () () TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
[#] M is non proper Element of K19( the carrier of M)
the finite open Element of K19( the carrier of M) is finite open Element of K19( the carrier of M)
C is finite open Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
A is finite open (M)
card A is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B is finite open (M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
[#] M is non empty non proper Element of K19( the carrier of M)
the carrier of M is non empty set
K19( the carrier of M) is non empty set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is finite open Element of K19( the carrier of M)
[#] M is non empty non proper Element of K19( the carrier of M)
B is finite open Element of K19( the carrier of M)
C is finite open (M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is Element of K19( the carrier of M)
(M,B) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is Element of K19( the carrier of M)
A \/ B is Element of K19( the carrier of M)
(M,(A \/ B)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ B } is set
A /\ B is Element of K19( the carrier of M)
(M,(A /\ B)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A /\ B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A /\ B } is set
(M,(A \/ B)) + (M,(A /\ B)) is V121() ext-real V125() set
(M,B) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
(M,A) + (M,B) is V121() ext-real V125() set
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e is finite open Element of K19( the carrier of M)
e /\ B is finite open Element of K19( the carrier of M)
c is set
{c} is non empty trivial finite 1 -element set
C \/ {c} is non empty finite set
b is finite open Element of K19( the carrier of M)
c is finite open Element of K19( the carrier of M)
c /\ B is finite open Element of K19( the carrier of M)
e /\ (c /\ B) is finite open Element of K19( the carrier of M)
e /\ c is finite open Element of K19( the carrier of M)
(e /\ c) /\ B is finite open Element of K19( the carrier of M)
e \/ (c /\ B) is finite Element of K19( the carrier of M)
b is set
{b} is non empty trivial finite 1 -element set
e \/ {b} is non empty finite set
D is finite open Element of K19( the carrier of M)
b is set
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card (c /\ B) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card c is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,A) + (card (c /\ B)) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
((M,A) + (card (c /\ B))) - (M,(A /\ B)) is V121() ext-real V125() set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
(M,A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B is Element of K19( the carrier of M)
A \/ B is Element of K19( the carrier of M)
(M,(A \/ B)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ B } is set
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {C} is non empty Element of K19( the carrier of M)
(M,(A \/ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
card {C} is non empty V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
A /\ {C} is finite Element of K19( the carrier of M)
(M,(A /\ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A /\ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A /\ {C} } is set
(M,(A \/ {C})) + (M,(A /\ {C})) is V121() ext-real V125() set
(M,{C}) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= {C} } is set
(M,A) + (M,{C}) is V121() ext-real V125() set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {B} is non empty Element of K19( the carrier of M)
(M,(A \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {C} is non empty Element of K19( the carrier of M)
(M,(A \/ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
{B,C} is non empty finite Element of K19( the carrier of M)
A \/ {B,C} is non empty Element of K19( the carrier of M)
(M,(A \/ {B,C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B,C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B,C} } is set
e is finite open Element of K19( the carrier of M)
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
c is finite open Element of K19( the carrier of M)
b is set
{b} is non empty trivial finite 1 -element set
e \/ {b} is non empty finite set
D is finite open Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {B} is non empty Element of K19( the carrier of M)
(M,(A \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of K19( the carrier of M)
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {C} is non empty Element of K19( the carrier of M)
(M,(A \/ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
e is finite open Element of K19( the carrier of M)
card e is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
B \/ {C} is non empty Element of K19( the carrier of M)
c is finite open Element of K19( the carrier of M)
c /\ (B \/ {C}) is finite open Element of K19( the carrier of M)
c /\ B is finite open Element of K19( the carrier of M)
c /\ {C} is finite open Element of K19( the carrier of M)
(c /\ B) \/ (c /\ {C}) is finite Element of K19( the carrier of M)
card {} is empty V31() V35() finite finite-membered cardinal {} -element V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() V227() Element of NAT
card {C} is non empty V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card (c /\ B) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,B) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
(card (c /\ B)) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,B) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
e \/ {C} is non empty finite Element of K19( the carrier of M)
(M,(B \/ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B \/ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B \/ {C} } is set
card c is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card (c /\ {C}) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card (c /\ B)) + (card (c /\ {C})) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
C is set
e is Element of the carrier of M
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {B} is non empty Element of K19( the carrier of M)
(M,(A \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
C is Element of the carrier of M
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
B is set
C is Element of the carrier of M
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
B is Element of K19( the carrier of M)
(M,B) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,B) } is set
C is set
e is Element of the carrier of M
e is Element of the carrier of M
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
(M,(M,A)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (M,A) } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (M,A) } is set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is finite open Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
C is finite open Element of K19( the carrier of M)
e is set
c is Element of the carrier of M
{c} is non empty trivial finite 1 -element Element of K19( the carrier of M)
B \/ {c} is non empty finite Element of K19( the carrier of M)
b is finite open Element of K19( the carrier of M)
A \/ {c} is non empty Element of K19( the carrier of M)
D is finite open Element of K19( the carrier of M)
(M,(A \/ {c})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {c} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {c} } is set
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
(M,A) \/ {B} is non empty Element of K19( the carrier of M)
(M,((M,A) \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (M,A) \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (M,A) \/ {B} } is set
(M,(M,A)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (M,A) } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (M,A) } is set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
C is finite open Element of K19( the carrier of M)
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,C) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= C } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= C } is set
A \/ {B} is non empty Element of K19( the carrier of M)
(M,(A \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
(M,(M,A)) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,(M,A)) } is set
B is set
C is Element of the carrier of M
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A) } is set
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {B} is non empty Element of K19( the carrier of M)
(M,(A \/ {B})) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A \/ {B}) } is set
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {C} is non empty Element of K19( the carrier of M)
(M,(A \/ {C})) is Element of K19( the carrier of M)
{ b₁ where b₁ is Element of the carrier of M : (M,b₁,A \/ {C}) } is set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
(M,(A \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {B} } is set
(M,A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(A \/ {B}) \/ {C} is non empty Element of K19( the carrier of M)
{B} \/ {C} is non empty finite Element of K19( the carrier of M)
A \/ ({B} \/ {C}) is non empty Element of K19( the carrier of M)
(M,(A \/ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ {C} } is set
(A \/ {C}) \/ {B} is non empty Element of K19( the carrier of M)
{C} \/ {B} is non empty finite Element of K19( the carrier of M)
A \/ ({C} \/ {B}) is non empty Element of K19( the carrier of M)
(M,((A \/ {C}) \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (A \/ {C}) \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (A \/ {C}) \/ {B} } is set
(M,((A \/ {B}) \/ {C})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (A \/ {B}) \/ {C} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (A \/ {B}) \/ {C} } is set
M is TopStruct
the carrier of M is set
K19( the carrier of M) is non empty set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
the Element of A is Element of A
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \ {C} is Element of K19( the carrier of M)
e is finite open Element of K19( the carrier of M)
e \/ {C} is non empty finite Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \ {B} is Element of K19( the carrier of M)
e is Element of K19( the carrier of M)
(A \ {B}) \/ {B} is non empty Element of K19( the carrier of M)
the Element of A is Element of A
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \ {C} is Element of K19( the carrier of M)
c is Element of the carrier of M
{c} is non empty trivial finite 1 -element set
A \ {c} is Element of K19( the carrier of M)
{c} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \ {c} is Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
(M,A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card A is V31() cardinal set
B is non empty finite Element of K19( the carrier of M)
the Element of B is Element of B
{ the Element of B} is non empty trivial finite 1 -element Element of K19(B)
K19(B) is non empty finite finite-membered set
B \ { the Element of B} is finite Element of K19( the carrier of M)
(M,B) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
card (B \ { the Element of B}) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(B \ { the Element of B}) \/ { the Element of B} is non empty finite set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of the carrier of M
{B} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \ {B} is Element of K19( the carrier of M)
C is finite open Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
card C is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(A \ {B}) \/ {B} is non empty Element of K19( the carrier of M)
(M,((A \ {B}) \/ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (A \ {B}) \/ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= (A \ {B}) \/ {B} } is set
(M,(A \ {B})) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \ {B} } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \ {B} } is set
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of K19( the carrier of M)
C is set
e is Element of the carrier of M
{e} is non empty trivial finite 1 -element Element of K19( the carrier of M)
B \ {e} is Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
B is finite open Element of K19( the carrier of M)
card B is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
C is set
e is Element of the carrier of M
{e} is non empty trivial finite 1 -element Element of K19( the carrier of M)
B \/ {e} is non empty finite Element of K19( the carrier of M)
c is V31() V35() finite cardinal V121() ext-real V125() set
c is V31() V35() finite cardinal V121() ext-real V125() set
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b \/ {e} is non empty finite Element of K19( the carrier of M)
b is finite open Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b \/ {e} is non empty finite Element of K19( the carrier of M)
D is Element of the carrier of M
{D} is non empty trivial finite 1 -element set
(b \/ {e}) \ {D} is finite Element of K19( the carrier of M)
{D} is non empty trivial finite 1 -element Element of K19( the carrier of M)
b \ {D} is finite open Element of K19( the carrier of M)
(b \ {D}) \/ {D} is non empty finite Element of K19( the carrier of M)
card (b \ {D}) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card (b \ {D})) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(b \/ {e}) \ {D} is finite Element of K19( the carrier of M)
(b \ {D}) \/ {e} is non empty finite Element of K19( the carrier of M)
Ae is finite open Element of K19( the carrier of M)
card Ae is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
Ae \/ {e} is non empty finite Element of K19( the carrier of M)
(b \/ {e}) \ {D} is finite Element of K19( the carrier of M)
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of K19( the carrier of M)
A /\ B is Element of K19( the carrier of M)
A \/ B is Element of K19( the carrier of M)
C is Element of the carrier of M
{C} is non empty trivial finite 1 -element Element of K19( the carrier of M)
(A \/ B) \ {C} is Element of K19( the carrier of M)
e is set
c is Element of the carrier of M
{c} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \ {c} is Element of K19( the carrier of M)
(M,(A \/ B)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A \/ B } is set
(M,(A /\ B)) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A /\ B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A /\ B } is set
(M,(A \/ B)) + (M,(A /\ B)) is V121() ext-real V125() set
(M,A) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= A } is set
(M,B) is V31() V35() finite cardinal V121() ext-real V125() set
{ (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
union { (card b₁) where b₁ is finite open Element of K19( the carrier of M) : b₁ c= B } is set
(M,A) + (M,B) is V121() ext-real V125() set
((M,(A \/ B)) + (M,(A /\ B))) + 1 is V121() ext-real V125() set
((M,A) + (M,B)) + 1 is V121() ext-real V125() set
b is finite Element of K19( the carrier of M)
D is finite Element of K19( the carrier of M)
b /\ D is finite Element of K19( the carrier of M)
card (b /\ D) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
x is Element of K19( the carrier of M)
x is finite open Element of K19( the carrier of M)
A \ {C} is Element of K19( the carrier of M)
B \ {C} is Element of K19( the carrier of M)
Be is finite open Element of K19( the carrier of M)
Be \/ {C} is non empty finite Element of K19( the carrier of M)
card D is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card Be is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card Be) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,B) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
Ae is finite open Element of K19( the carrier of M)
Ae \/ {C} is non empty finite Element of K19( the carrier of M)
card b is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card Ae is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card Ae) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(M,A) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
b \/ D is finite Element of K19( the carrier of M)
card (b \/ D) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card (b \/ D)) + (card (b /\ D)) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
((M,A) + 1) + ((M,B) + 1) is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(((M,A) + (M,B)) + 1) + 1 is V121() ext-real V125() set
(((M,(A \/ B)) + (M,(A /\ B))) + 1) + 1 is V121() ext-real V125() set
x \/ {C} is non empty finite Element of K19( the carrier of M)
D is Element of K19( the carrier of M)
(M,(A \/ B)) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
card x is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
(card x) + 1 is V31() V35() finite cardinal V121() ext-real V125() V171() V210() V221() V222() V223() V224() V225() V226() Element of NAT
M is non empty non void () () () () TopStruct
the carrier of M is non empty set
K19( the carrier of M) is non empty set
A is Element of K19( the carrier of M)
B is Element of K19( the carrier of M)
C is Element of K19( the carrier of M)
e is Element of the carrier of M
{e} is non empty trivial finite 1 -element Element of K19( the carrier of M)
A \/ {e} is non empty Element of K19( the carrier of M)
c is set
b is set
B /\ C is Element of K19( the carrier of M)
B \/ C is Element of K19( the carrier of M)
(B \/ C) \ {e} is Element of K19( the carrier of M)
D is Element of K19( the carrier of M)
x is set