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

( not b

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

( not b

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

( not b

{} (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

( not b

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

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

{} 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

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

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

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

union { (card b

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

union { (card b

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

union { (card b

{} 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

union { (card b

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

union { (card b

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

union { (card b

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

union { (card b

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

union { (card b

B is Element of K19( the carrier of M)

(M,B) is V31() V35() finite cardinal V121() ext-real V125() set

{ (card b

union { (card b

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

union { (card b

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

union { (card b

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

union { (card b

(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

union { (card b

(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

union { (card b

(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

union { (card b

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

union { (card b

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

union { (card b

(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

union { (card b

(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

union { (card b

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

union { (card b

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

union { (card b

{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

union { (card b

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

union { (card b

(M,A) is V31() V35() finite cardinal V121() ext-real V125() set

{ (card b

union { (card b

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

union { (card b

(M,A) is V31() V35() finite cardinal V121() ext-real V125() set

{ (card b

union { (card b

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

union { (card b

(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

union { (card b

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

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

(M,A) is V31() V35() finite cardinal V121() ext-real V125() set

{ (card b

union { (card b

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

union { (card b

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

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

B is Element of K19( the carrier of M)

(M,B) is Element of K19( the carrier of M)

{ b

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

(M,(M,A)) is V31() V35() finite cardinal V121() ext-real V125() set

{ (card b

union { (card b

(M,A) is V31() V35() finite cardinal V121() ext-real V125() set

{ (card b

union { (card b

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

union { (card b

card D is V31() V35() finite cardinal V121() ext-real