:: SIMPLEX1 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal non empty-membered Element of bool REAL

bool REAL is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of NAT

- 1 is non empty V21() V29() ext-real non positive negative set

K87(1) is non empty V21() V29() V30() ext-real non positive negative finite set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[:NAT,NAT:] is Relation-like non empty non trivial non finite non empty-membered set

[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite non empty-membered set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite V47() subset-closed non with_non-empty_elements non empty-membered V290() d.union-closed set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal non empty-membered set

bool omega is non empty non trivial non finite V47() subset-closed non with_non-empty_elements non empty-membered V290() d.union-closed set

bool NAT is non empty non trivial non finite V47() subset-closed non with_non-empty_elements non empty-membered V290() d.union-closed set

{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() V30() ext-real non positive non negative finite finite-yielding finite-membered cardinal {} -element V47() V50() V51() V52() V53() subset-closed Function-yielding V197() set

the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() V30() ext-real non positive non negative finite finite-yielding finite-membered cardinal {} -element V47() V50() V51() V52() V53() subset-closed Function-yielding V197() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() V30() ext-real non positive non negative finite finite-yielding finite-membered cardinal {} -element V47() V50() V51() V52() V53() subset-closed Function-yielding V197() set

2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of NAT

K469() is set

{{}} is functional non empty trivial finite finite-membered 1 -element V47() subset-closed non with_non-empty_elements V290() d.union-closed set

K272({{}}) is M10({{}})

[:K272({{}}),{{}}:] is Relation-like set

bool [:K272({{}}),{{}}:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

K36(K272({{}}),{{}}) is set

K620() is TopStruct

the carrier of K620() is set

0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() V30() ext-real non positive non negative finite finite-yielding finite-membered cardinal {} -element V47() V50() V51() V52() V53() subset-closed Function-yielding V197() Element of NAT

- 1 is non empty V21() V29() V30() ext-real non positive negative finite Element of REAL

+infty is non empty V29() ext-real positive non negative set

-infty is non empty V29() ext-real non positive negative set

union {} is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

k is set

card k is epsilon-transitive epsilon-connected ordinal cardinal set

V is Relation-like set

card V is epsilon-transitive epsilon-connected ordinal cardinal set

dom V is set

(dom V) \ k is Element of bool (dom V)

bool (dom V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

V | ((dom V) \ k) is Relation-like set

card (V | ((dom V) \ k)) is epsilon-transitive epsilon-connected ordinal cardinal set

Aff is epsilon-transitive epsilon-connected ordinal cardinal set

Aff *` (card k) is epsilon-transitive epsilon-connected ordinal cardinal set

(card (V | ((dom V) \ k))) +` (Aff *` (card k)) is epsilon-transitive epsilon-connected ordinal cardinal set

XX is Relation-like Function-like set

dom XX is set

x is set

XX . x is set

Im (V,x) is set

card (Im (V,x)) is epsilon-transitive epsilon-connected ordinal cardinal set

C is Relation-like Function-like set

dom C is set

rng C is set

x is Relation-like Function-like set

dom x is set

C is set

x . C is set

XX . C is set

F is Relation-like Function-like set

dom F is set

rng F is set

C is Relation-like Function-like Function-yielding V197() set

V | k is Relation-like set

F is Relation-like Function-like set

dom F is set

rng F is set

[:k,Aff:] is Relation-like set

X is set

A1 is set

F . A1 is set

A1 `1 is set

C . (A1 `1) is Relation-like Function-like set

A1 `2 is set

(C . (A1 `1)) . (A1 `2) is set

[(A1 `1),((C . (A1 `1)) . (A1 `2))] is V15() set

{(A1 `1),((C . (A1 `1)) . (A1 `2))} is non empty finite set

{(A1 `1)} is non empty trivial finite 1 -element set

{{(A1 `1),((C . (A1 `1)) . (A1 `2))},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

[(A1 `1),(A1 `2)] is V15() set

{(A1 `1),(A1 `2)} is non empty finite set

{{(A1 `1),(A1 `2)},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

V .: {(A1 `1)} is set

XX . (A1 `1) is set

S is Relation-like Function-like set

dom S is set

rng S is set

Im (V,(A1 `1)) is set

S . (A1 `2) is set

X is set

A1 is set

S is set

[A1,S] is V15() set

{A1,S} is non empty finite set

{A1} is non empty trivial finite 1 -element set

{{A1,S},{A1}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

C . A1 is Relation-like Function-like set

XX . A1 is set

CA is Relation-like Function-like set

dom CA is set

rng CA is set

F is set

CA . F is set

[A1,F] is V15() set

{A1,F} is non empty finite set

{{A1,F},{A1}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

[A1,F] `1 is set

C . ([A1,F] `1) is Relation-like Function-like set

[A1,F] `2 is set

(C . ([A1,F] `1)) . ([A1,F] `2) is set

[([A1,F] `1),((C . ([A1,F] `1)) . ([A1,F] `2))] is V15() set

{([A1,F] `1),((C . ([A1,F] `1)) . ([A1,F] `2))} is non empty finite set

{([A1,F] `1)} is non empty trivial finite 1 -element set

{{([A1,F] `1),((C . ([A1,F] `1)) . ([A1,F] `2))},{([A1,F] `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

Im (V,A1) is set

F . [A1,F] is set

X is set

A1 is set

F . X is set

F . A1 is set

X `1 is set

C . (X `1) is Relation-like Function-like set

X `2 is set

(C . (X `1)) . (X `2) is set

[(X `1),((C . (X `1)) . (X `2))] is V15() set

{(X `1),((C . (X `1)) . (X `2))} is non empty finite set

{(X `1)} is non empty trivial finite 1 -element set

{{(X `1),((C . (X `1)) . (X `2))},{(X `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

A1 `1 is set

C . (A1 `1) is Relation-like Function-like set

A1 `2 is set

(C . (A1 `1)) . (A1 `2) is set

[(A1 `1),((C . (A1 `1)) . (A1 `2))] is V15() set

{(A1 `1),((C . (A1 `1)) . (A1 `2))} is non empty finite set

{(A1 `1)} is non empty trivial finite 1 -element set

{{(A1 `1),((C . (A1 `1)) . (A1 `2))},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

[(X `1),(X `2)] is V15() set

{(X `1),(X `2)} is non empty finite set

{{(X `1),(X `2)},{(X `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

Im (V,(X `1)) is set

[(A1 `1),(A1 `2)] is V15() set

{(A1 `1),(A1 `2)} is non empty finite set

{{(A1 `1),(A1 `2)},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

Im (V,(A1 `1)) is set

XX . (A1 `1) is set

S is Relation-like Function-like set

dom S is set

rng S is set

XX . (X `1) is set

CA is Relation-like Function-like set

dom CA is set

rng CA is set

CA . (X `2) is set

S . (A1 `2) is set

card (V | k) is epsilon-transitive epsilon-connected ordinal cardinal set

card [:k,Aff:] is epsilon-transitive epsilon-connected ordinal cardinal set

[:(card k),Aff:] is Relation-like set

card [:(card k),Aff:] is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

A1 is set

S is set

[A1,S] is V15() set

{A1,S} is non empty finite set

{A1} is non empty trivial finite 1 -element set

{{A1,S},{A1}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

((dom V) \ k) \/ k is set

(dom V) \/ k is set

(V | k) \/ (V | ((dom V) \ k)) is Relation-like set

V | (dom V) is Relation-like set

XX is set

Im (V,XX) is set

x is set

[XX,x] is V15() set

{XX,x} is non empty finite set

{XX} is non empty trivial finite 1 -element set

{{XX,x},{XX}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

card {} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() V30() ext-real non positive non negative finite finite-yielding finite-membered cardinal {} -element V47() V50() V51() V52() V53() subset-closed Function-yielding V197() Element of omega

x is set

Im (V,x) is set

card (Im (V,x)) is epsilon-transitive epsilon-connected ordinal cardinal set

C is set

[x,C] is V15() set

{x,C} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,C},{x}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

k is set

card k is epsilon-transitive epsilon-connected ordinal cardinal set

V is non empty finite set

card V is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of omega

(card V) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

[:k,V:] is Relation-like set

bool [:k,V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(card V) - 1 is V21() V29() V30() ext-real finite Element of REAL

XX is Relation-like k -defined V -valued Function-like quasi_total Element of bool [:k,V:]

rng XX is finite Element of bool V

bool V is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is non empty finite set

[:Aff,V:] is Relation-like non empty finite set

bool [:Aff,V:] is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

dom XX is Element of bool k

bool k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

x is Relation-like Aff -defined V -valued Function-like quasi_total finite Element of bool [:Aff,V:]

C is set

{C} is non empty trivial finite 1 -element set

x " {C} is finite Element of bool Aff

bool Aff is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

card (x " {C}) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

C is set

{C} is non empty trivial finite 1 -element set

x " {C} is finite Element of bool Aff

bool Aff is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

card (x " {C}) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

C is set

{C} is non empty trivial finite 1 -element set

x " {C} is finite Element of bool Aff

bool Aff is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

card (x " {C}) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

(dom XX) \ (x " {C}) is Element of bool k

x | ((dom XX) \ (x " {C})) is Relation-like Aff -defined (dom XX) \ (x " {C}) -defined Aff -defined V -valued Function-like finite Element of bool [:Aff,V:]

XX " {C} is Element of bool k

card (XX " {C}) is epsilon-transitive epsilon-connected ordinal cardinal set

1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

dom (x | ((dom XX) \ (x " {C}))) is finite Element of bool Aff

card (dom (x | ((dom XX) \ (x " {C})))) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

card Aff is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of omega

(card Aff) - (card (x " {C})) is V21() V29() ext-real set

- (card (x " {C})) is V21() V29() ext-real non positive set

K87((card (x " {C}))) is V21() V29() V30() ext-real non positive finite set

(card Aff) + (- (card (x " {C}))) is V21() V29() ext-real set

K85((card Aff),(- (card (x " {C})))) is V21() V29() ext-real set

K89((card Aff),(card (x " {C}))) is V21() V29() V30() ext-real finite set

V \ {C} is finite Element of bool V

rng (x | ((dom XX) \ (x " {C}))) is finite Element of bool V

[:(dom (x | ((dom XX) \ (x " {C})))),(V \ {C}):] is Relation-like finite set

bool [:(dom (x | ((dom XX) \ (x " {C})))),(V \ {C}):] is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of NAT

F + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

card (V \ {C}) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

(card V) + (- 1) is V21() V29() V30() ext-real finite Element of REAL

1 - (card (x " {C})) is V21() V29() V30() ext-real finite Element of REAL

(card V) + (1 - (card (x " {C}))) is V21() V29() V30() ext-real finite Element of REAL

1 - (- 1) is non empty V21() V29() V30() ext-real positive non negative finite Element of REAL

CA is set

{CA} is non empty trivial finite 1 -element set

XX " {CA} is Element of bool k

card (XX " {CA}) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Relation-like dom (x | ((dom XX) \ (x " {C}))) -defined V \ {C} -valued Function-like quasi_total finite Element of bool [:(dom (x | ((dom XX) \ (x " {C})))),(V \ {C}):]

rng S is finite Element of bool (V \ {C})

bool (V \ {C}) is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

S " {CA} is finite Element of bool (dom (x | ((dom XX) \ (x " {C}))))

bool (dom (x | ((dom XX) \ (x " {C})))) is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is set

{F} is non empty trivial finite 1 -element set

k is 1-sorted

the carrier of k is set

V is SimplicialComplexStr of the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is Element of bool the carrier of V

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

k is 1-sorted

the carrier of k is set

V is SimplicialComplexStr of the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is Element of bool (bool the carrier of V)

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

bool ([#] V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool ([#] V))

bool ([#] V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool ([#] V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

k is 1-sorted

the carrier of k is set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

V is subset-closed SimplicialComplexStr of the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is finite Element of bool the carrier of V

(k,V,Aff) is Element of bool the carrier of k

{(k,V,Aff)} is non empty trivial finite 1 -element Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Complex_of {(k,V,Aff)} is strict non void subset-closed non with_non-empty_elements total SimplicialComplexStr of the carrier of k

subset-closed_closure_of {(k,V,Aff)} is non empty V47() subset-closed non with_non-empty_elements Element of bool (bool the carrier of k)

TopStruct(# the carrier of k,(subset-closed_closure_of {(k,V,Aff)}) #) is strict TopStruct

the topology of V is Element of bool (bool the carrier of V)

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

{Aff} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)

[#] (Complex_of {(k,V,Aff)}) is non proper Element of bool the carrier of (Complex_of {(k,V,Aff)})

the carrier of (Complex_of {(k,V,Aff)}) is set

bool the carrier of (Complex_of {(k,V,Aff)}) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

the_family_of V is V47() subset-closed Element of bool (bool the carrier of V)

the topology of (Complex_of {(k,V,Aff)}) is Element of bool (bool the carrier of (Complex_of {(k,V,Aff)}))

bool (bool the carrier of (Complex_of {(k,V,Aff)})) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

k is non empty RLSStruct

the carrier of k is non empty set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

V is SimplicialComplexStr of the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

{ (conv (k,V,b

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is set

XX is Element of bool the carrier of V

(k,V,XX) is Element of bool the carrier of k

conv (k,V,XX) is convex Element of bool the carrier of k

F is Element of bool (bool the carrier of k)

union F is Element of bool the carrier of k

XX is Element of bool the carrier of k

x is set

C is set

F is Element of bool the carrier of V

(k,V,F) is Element of bool the carrier of k

conv (k,V,F) is convex Element of bool the carrier of k

X is Element of bool the carrier of V

(k,V,X) is Element of bool the carrier of k

conv (k,V,X) is convex Element of bool the carrier of k

C is Element of bool the carrier of V

(k,V,C) is Element of bool the carrier of k

conv (k,V,C) is convex Element of bool the carrier of k

Aff is Element of bool the carrier of k

F is Element of bool the carrier of k

XX is set

x is Element of bool the carrier of V

(k,V,x) is Element of bool the carrier of k

conv (k,V,x) is convex Element of bool the carrier of k

x is Element of bool the carrier of V

(k,V,x) is Element of bool the carrier of k

conv (k,V,x) is convex Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

the topology of V is Element of bool (bool the carrier of V)

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is SimplicialComplexStr of the carrier of k

the topology of Aff is Element of bool (bool the carrier of Aff)

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,Aff) is Element of bool the carrier of k

F is set

XX is Element of bool the carrier of V

(k,V,XX) is Element of bool the carrier of k

conv (k,V,XX) is convex Element of bool the carrier of k

x is Element of bool the carrier of Aff

(k,Aff,x) is Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is Element of bool the carrier of V

(k,V,Aff) is Element of bool the carrier of k

conv (k,V,Aff) is convex Element of bool the carrier of k

F is set

k is set

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is subset-closed SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is Element of bool the carrier of Aff

(V,Aff,F) is Element of bool the carrier of V

conv (V,Aff,F) is convex Element of bool the carrier of V

{ (Int b

union { (Int b

XX is set

x is Element of bool the carrier of V

Int x is Element of bool the carrier of V

C is Element of bool the carrier of Aff

the topology of Aff is Element of bool (bool the carrier of Aff)

bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is Element of bool the carrier of Aff

(V,Aff,F) is Element of bool the carrier of V

Int (V,Aff,F) is Element of bool the carrier of V

F is Element of bool the carrier of Aff

(V,Aff,F) is Element of bool the carrier of V

Int (V,Aff,F) is Element of bool the carrier of V

conv (V,Aff,F) is convex Element of bool the carrier of V

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of V is Element of bool (bool the carrier of V)

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is non empty set

F is Element of bool the carrier of V

(k,V,F) is Element of bool the carrier of k

conv (k,V,F) is convex Element of bool the carrier of k

XX is set

Aff is set

F is Element of bool the carrier of V

(k,V,F) is Element of bool the carrier of k

conv (k,V,F) is convex Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

V is Element of bool the carrier of k

{V} is non empty trivial finite 1 -element Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Complex_of {V} is strict non void subset-closed non with_non-empty_elements total SimplicialComplexStr of the carrier of k

subset-closed_closure_of {V} is non empty V47() subset-closed non with_non-empty_elements Element of bool (bool the carrier of k)

TopStruct(# the carrier of k,(subset-closed_closure_of {V}) #) is strict TopStruct

(k,(Complex_of {V})) is Element of bool the carrier of k

conv V is convex Element of bool the carrier of k

the carrier of (Complex_of {V}) is set

bool the carrier of (Complex_of {V}) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of (Complex_of {V}) is Element of bool (bool the carrier of (Complex_of {V}))

bool (bool the carrier of (Complex_of {V})) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool V)

bool V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

XX is set

x is Element of bool the carrier of (Complex_of {V})

(k,(Complex_of {V}),x) is Element of bool the carrier of k

conv (k,(Complex_of {V}),x) is convex Element of bool the carrier of k

F is Element of bool the carrier of (Complex_of {V})

(k,(Complex_of {V}),F) is Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

V is Element of bool (bool the carrier of k)

Aff is Element of bool (bool the carrier of k)

V \/ Aff is Element of bool (bool the carrier of k)

Complex_of (V \/ Aff) is strict subset-closed total SimplicialComplexStr of the carrier of k

subset-closed_closure_of (V \/ Aff) is V47() subset-closed Element of bool (bool the carrier of k)

TopStruct(# the carrier of k,(subset-closed_closure_of (V \/ Aff)) #) is strict TopStruct

(k,(Complex_of (V \/ Aff))) is Element of bool the carrier of k

Complex_of V is strict subset-closed total SimplicialComplexStr of the carrier of k

subset-closed_closure_of V is V47() subset-closed Element of bool (bool the carrier of k)

TopStruct(# the carrier of k,(subset-closed_closure_of V) #) is strict TopStruct

(k,(Complex_of V)) is Element of bool the carrier of k

Complex_of Aff is strict subset-closed total SimplicialComplexStr of the carrier of k

subset-closed_closure_of Aff is V47() subset-closed Element of bool (bool the carrier of k)

TopStruct(# the carrier of k,(subset-closed_closure_of Aff) #) is strict TopStruct

(k,(Complex_of Aff)) is Element of bool the carrier of k

(k,(Complex_of V)) \/ (k,(Complex_of Aff)) is Element of bool the carrier of k

the topology of (Complex_of V) is Element of bool (bool the carrier of (Complex_of V))

the carrier of (Complex_of V) is set

bool the carrier of (Complex_of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of (Complex_of V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of (Complex_of Aff) is Element of bool (bool the carrier of (Complex_of Aff))

the carrier of (Complex_of Aff) is set

bool the carrier of (Complex_of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of (Complex_of Aff)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of (Complex_of V) \/ the topology of (Complex_of Aff) is set

the topology of (Complex_of (V \/ Aff)) is Element of bool (bool the carrier of (Complex_of (V \/ Aff)))

the carrier of (Complex_of (V \/ Aff)) is set

bool the carrier of (Complex_of (V \/ Aff)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of (Complex_of (V \/ Aff))) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

C is set

F is Element of bool the carrier of (Complex_of (V \/ Aff))

(k,(Complex_of (V \/ Aff)),F) is Element of bool the carrier of k

conv (k,(Complex_of (V \/ Aff)),F) is convex Element of bool the carrier of k

X is Element of bool the carrier of (Complex_of V)

(k,(Complex_of V),X) is Element of bool the carrier of k

X is Element of bool the carrier of (Complex_of Aff)

(k,(Complex_of Aff),X) is Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is Element of bool the carrier of V

(k,V,Aff) is Element of bool the carrier of k

conv (k,V,Aff) is convex Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is (k,V)

(k,Aff) is Element of bool the carrier of k

F is set

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

XX is Element of bool the carrier of Aff

(k,Aff,XX) is Element of bool the carrier of k

conv (k,Aff,XX) is convex Element of bool the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

x is Element of bool the carrier of V

(k,V,x) is Element of bool the carrier of k

conv (k,V,x) is convex Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is non void non empty-membered SimplicialComplexStr of the carrier of k

Aff is (k,V)

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,Aff) is Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is Element of bool the carrier of V

(k,V,Aff) is Element of bool the carrier of k

conv (k,V,Aff) is convex Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

the carrier of V is set

the topology of V is Element of bool (bool the carrier of V)

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Complex_of the topology of V is strict subset-closed total SimplicialComplexStr of the carrier of V

subset-closed_closure_of the topology of V is V47() subset-closed Element of bool (bool the carrier of V)

TopStruct(# the carrier of V,(subset-closed_closure_of the topology of V) #) is strict TopStruct

[#] (Complex_of the topology of V) is non proper Element of bool the carrier of (Complex_of the topology of V)

the carrier of (Complex_of the topology of V) is set

bool the carrier of (Complex_of the topology of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

XX is SimplicialComplexStr of the carrier of k

(k,XX) is Element of bool the carrier of k

x is set

C is Element of bool the carrier of V

(k,V,C) is Element of bool the carrier of k

conv (k,V,C) is convex Element of bool the carrier of k

the carrier of XX is set

bool the carrier of XX is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of XX is Element of bool (bool the carrier of XX)

bool (bool the carrier of XX) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is Element of bool the carrier of XX

(k,XX,F) is Element of bool the carrier of k

the carrier of XX is set

bool the carrier of XX is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

x is Element of bool the carrier of XX

(k,XX,x) is Element of bool the carrier of k

conv (k,XX,x) is convex Element of bool the carrier of k

the topology of XX is Element of bool (bool the carrier of XX)

bool (bool the carrier of XX) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

C is set

F is Element of bool the carrier of V

(k,V,F) is Element of bool the carrier of k

conv (k,V,F) is convex Element of bool the carrier of k

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is subset-closed SimplicialComplexStr of the carrier of k

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of V is Element of bool (bool the carrier of V)

Sub_of_Fin the topology of V is finite-membered Element of bool the topology of V

bool the topology of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is Element of bool (bool the carrier of V)

Complex_of F is strict subset-closed total SimplicialComplexStr of the carrier of V

subset-closed_closure_of F is V47() subset-closed Element of bool (bool the carrier of V)

TopStruct(# the carrier of V,(subset-closed_closure_of F) #) is strict TopStruct

[#] (Complex_of F) is non proper Element of bool the carrier of (Complex_of F)

the carrier of (Complex_of F) is set

bool the carrier of (Complex_of F) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

the_family_of V is V47() subset-closed Element of bool (bool the carrier of V)

x is SimplicialComplexStr of the carrier of k

the topology of x is Element of bool (bool the carrier of x)

the carrier of x is set

bool the carrier of x is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of x) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,x) is Element of bool the carrier of k

C is set

F is Element of bool the carrier of V

(k,V,F) is Element of bool the carrier of k

conv (k,V,F) is convex Element of bool the carrier of k

X is non empty Element of bool the carrier of k

ConvexComb k is set

{ (Sum b

A1 is Relation-like the carrier of k -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of X

Sum A1 is Element of the carrier of k

Carrier A1 is finite Element of bool the carrier of k

{ b

S is non empty Element of bool the carrier of k

CA is Element of bool the carrier of x

F is Relation-like the carrier of k -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of S

{ (Sum b

conv S is non empty convex Element of bool the carrier of k

(k,x,CA) is Element of bool the carrier of k

C is Element of bool the carrier of x

(k,x,C) is Element of bool the carrier of k

conv (k,x,C) is convex Element of bool the carrier of k

F is Element of bool the carrier of V

(k,V,F) is Element of bool the carrier of k

k is non empty RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

Aff is (k,V)

F is (k,Aff)

(k,F) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,Aff) is Element of bool the carrier of k

(k,V) is Element of bool the carrier of k

the carrier of F is set

bool the carrier of F is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

XX is Element of bool the carrier of F

(k,F,XX) is Element of bool the carrier of k

conv (k,F,XX) is convex Element of bool the carrier of k

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

x is Element of bool the carrier of Aff

(k,Aff,x) is Element of bool the carrier of k

conv (k,Aff,x) is convex Element of bool the carrier of k

C is Element of bool the carrier of V

(k,V,C) is Element of bool the carrier of k

conv (k,V,C) is convex Element of bool the carrier of k

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is SimplicialComplexStr of the carrier of k

the carrier of V is set

the topology of V is Element of bool (bool the carrier of V)

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Complex_of the topology of V is strict subset-closed total SimplicialComplexStr of the carrier of V

subset-closed_closure_of the topology of V is V47() subset-closed Element of bool (bool the carrier of V)

TopStruct(# the carrier of V,(subset-closed_closure_of the topology of V) #) is strict TopStruct

Aff is (k,V)

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of Aff is Element of bool (bool the carrier of Aff)

Sub_of_Fin the topology of Aff is finite-membered Element of bool the topology of Aff

bool the topology of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is Element of bool (bool the carrier of Aff)

Complex_of F is strict subset-closed total SimplicialComplexStr of the carrier of Aff

subset-closed_closure_of F is V47() subset-closed Element of bool (bool the carrier of Aff)

TopStruct(# the carrier of Aff,(subset-closed_closure_of F) #) is strict TopStruct

XX is (k,V)

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

BOOL the carrier of k is set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of k) \ {{}} is Element of bool (bool the carrier of k)

[:(BOOL the carrier of k), the carrier of k:] is Relation-like set

bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

[#] V is non proper Element of bool the carrier of V

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]

subdivision (Aff,V) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the carrier of (subdivision (Aff,V)) is set

bool the carrier of (subdivision (Aff,V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

dom Aff is Element of bool (BOOL the carrier of k)

bool (BOOL the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

XX is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

XX + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

x is set

C is finite non dependent Element of bool the carrier of V

(k,V,C) is Element of bool the carrier of k

conv (k,V,C) is convex Element of bool the carrier of k

card C is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

{C} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)

union {C} is finite Element of bool the carrier of V

X is Element of bool the carrier of V

F is non empty Element of bool the carrier of k

Aff . F is set

Aff . C is set

Aff .: {C} is finite Element of bool the carrier of k

Im (Aff,C) is set

X is Element of the carrier of k

{X} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

conv F is non empty convex Element of bool the carrier of k

[#] (subdivision (Aff,V)) is non proper Element of bool the carrier of (subdivision (Aff,V))

S is set

CA is set

S is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)

Aff .: S is finite Element of bool the carrier of k

union S is finite Element of bool the carrier of V

A1 is Element of bool the carrier of (subdivision (Aff,V))

(k,(subdivision (Aff,V)),A1) is Element of bool the carrier of k

conv (k,(subdivision (Aff,V)),A1) is convex Element of bool the carrier of k

conv {X} is non empty convex Element of bool the carrier of k

S is Element of the carrier of k

CA is Element of the carrier of k

{S} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

F \ {S} is Element of bool the carrier of k

conv (F \ {S}) is convex Element of bool the carrier of k

F is V21() V29() ext-real Element of REAL

F * X is Element of the carrier of k

1 - F is V21() V29() ext-real Element of REAL

(1 - F) * CA is Element of the carrier of k

(F * X) + ((1 - F) * CA) is Element of the carrier of k

C \ {S} is finite non dependent Element of bool the carrier of V

(k,V,(C \ {S})) is Element of bool the carrier of k

card (C \ {S}) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

XX is Element of bool the carrier of (subdivision (Aff,V))

XX is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)

Aff .: XX is finite Element of bool the carrier of k

(k,(subdivision (Aff,V)),XX) is Element of bool the carrier of k

conv (k,(subdivision (Aff,V)),XX) is convex Element of bool the carrier of k

union XX is finite Element of bool the carrier of V

XX \/ {C} is non empty finite finite-membered Element of bool (bool the carrier of V)

XXA is set

m1 is set

XXA is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)

Aff .: XXA is finite Element of bool the carrier of k

A1 is Element of bool the carrier of (subdivision (Aff,V))

XX \/ A1 is Element of bool the carrier of (subdivision (Aff,V))

m1 is Element of bool the carrier of (subdivision (Aff,V))

(k,(subdivision (Aff,V)),m1) is Element of bool the carrier of k

conv (k,(subdivision (Aff,V)),m1) is convex Element of bool the carrier of k

union XXA is finite Element of bool the carrier of V

(union XX) \/ C is finite Element of bool the carrier of V

XX is set

x is finite non dependent Element of bool the carrier of V

(k,V,x) is Element of bool the carrier of k

conv (k,V,x) is convex Element of bool the carrier of k

card x is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

(k,(subdivision (Aff,V))) is Element of bool the carrier of k

XX is set

x is Element of bool the carrier of V

(k,V,x) is Element of bool the carrier of k

conv (k,V,x) is convex Element of bool the carrier of k

C is finite non dependent Element of bool the carrier of V

card C is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

F is set

X is finite non dependent Element of bool the carrier of V

(k,V,X) is Element of bool the carrier of k

conv (k,V,X) is convex Element of bool the carrier of k

card X is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

X is Element of bool the carrier of (subdivision (Aff,V))

F is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)

Aff .: F is finite Element of bool the carrier of k

(k,(subdivision (Aff,V)),X) is Element of bool the carrier of k

conv (k,(subdivision (Aff,V)),X) is convex Element of bool the carrier of k

union F is finite Element of bool the carrier of V

XX is Element of bool the carrier of (subdivision (Aff,V))

(k,(subdivision (Aff,V)),XX) is Element of bool the carrier of k

conv (k,(subdivision (Aff,V)),XX) is convex Element of bool the carrier of k

x is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)

Aff .: x is finite Element of bool the carrier of k

{} V is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() V30() ext-real non positive non negative finite finite-yielding finite-membered cardinal {} -element V47() V50() V51() V52() V53() non dependent subset-closed Function-yielding V197() Element of bool the carrier of V

(k,V,({} V)) is Element of bool the carrier of k

conv (k,V,({} V)) is convex Element of bool the carrier of k

union x is finite Element of bool the carrier of V

C is finite Element of bool the carrier of V

(k,V,C) is Element of bool the carrier of k

conv (k,V,C) is convex Element of bool the carrier of k

F is set

X is set

Aff . X is set

A1 is finite non dependent Element of bool the carrier of V

Aff . A1 is set

(k,V,A1) is Element of bool the carrier of k

conv (k,V,A1) is convex Element of bool the carrier of k

XX is Element of bool the carrier of (subdivision (Aff,V))

(k,(subdivision (Aff,V)),XX) is Element of bool the carrier of k

conv (k,(subdivision (Aff,V)),XX) is convex Element of bool the carrier of k

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

Aff is subset-closed finite-membered (k,V)

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]

BOOL the carrier of k is set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of k) \ {{}} is Element of bool (bool the carrier of k)

[:(BOOL the carrier of k), the carrier of k:] is Relation-like set

bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision ((center_of_mass k),V) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

F is finite non dependent Element of bool the carrier of V

(center_of_mass k) . F is set

(k,V,F) is Element of bool the carrier of k

conv (k,V,F) is convex Element of bool the carrier of k

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] Aff is non proper Element of bool the carrier of Aff

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]

BOOL the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)

[:(BOOL the carrier of V), the carrier of V:] is Relation-like set

bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

k is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

subdivision (k,(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

F is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

subdivision (F,(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

F + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

subdivision ((F + 1),(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

XX is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

(V,XX) is Element of bool the carrier of V

[#] XX is non proper Element of bool the carrier of XX

the carrier of XX is set

bool the carrier of XX is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision (1,(center_of_mass V),(subdivision (F,(center_of_mass V),Aff))) is SimplicialComplexStr of the carrier of V

subdivision ((center_of_mass V),XX) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,XX) is non void subset-closed finite-membered non with_non-empty_elements (V,XX)

subdivision ({},(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

({},k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)

center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]

BOOL the carrier of k is set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of k) \ {{}} is Element of bool (bool the carrier of k)

[:(BOOL the carrier of k), the carrier of k:] is Relation-like set

bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision ({},(center_of_mass k),V) is SimplicialComplexStr of the carrier of k

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(1,k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)

(k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)

center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]

BOOL the carrier of k is set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of k) \ {{}} is Element of bool (bool the carrier of k)

[:(BOOL the carrier of k), the carrier of k:] is Relation-like set

bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision (1,(center_of_mass k),V) is SimplicialComplexStr of the carrier of k

subdivision ((center_of_mass k),V) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

k is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] Aff is non proper Element of bool the carrier of Aff

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

[#] (k,V,Aff) is non proper Element of bool the carrier of (k,V,Aff)

the carrier of (k,V,Aff) is set

bool the carrier of (k,V,Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]

BOOL the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)

[:(BOOL the carrier of V), the carrier of V:] is Relation-like set

bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision (k,(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] Aff is non proper Element of bool the carrier of Aff

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

k is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

(V,(k,V,Aff)) is Element of bool the carrier of V

k is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

k + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] Aff is non proper Element of bool the carrier of Aff

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

((k + 1),V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

(V,(k,V,Aff)) is non void subset-closed finite-membered non with_non-empty_elements (V,(k,V,Aff))

(V,(k,V,Aff)) is Element of bool the carrier of V

[#] (k,V,Aff) is non proper Element of bool the carrier of (k,V,Aff)

the carrier of (k,V,Aff) is set

bool the carrier of (k,V,Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]

BOOL the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)

[:(BOOL the carrier of V), the carrier of V:] is Relation-like set

bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

1 + k is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

subdivision ((1 + k),(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

subdivision (k,(center_of_mass V),Aff) is SimplicialComplexStr of the carrier of V

subdivision (1,(center_of_mass V),(subdivision (k,(center_of_mass V),Aff))) is SimplicialComplexStr of the carrier of V

subdivision (1,(center_of_mass V),(k,V,Aff)) is SimplicialComplexStr of the carrier of V

(1,V,(k,V,Aff)) is non void subset-closed finite-membered non with_non-empty_elements (V,(k,V,Aff))

k is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of k is non empty set

V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

(k,V) is Element of bool the carrier of k

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] V is non proper Element of bool the carrier of V

the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

degree V is ext-real set

the topology of V is Element of bool (bool the carrier of V)

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

TopStruct(# the carrier of V, the topology of V #) is strict TopStruct

(k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)

center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]

BOOL the carrier of k is set

bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)

bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of k) \ {{}} is Element of bool (bool the carrier of k)

[:(BOOL the carrier of k), the carrier of k:] is Relation-like set

bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision ((center_of_mass k),V) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k

[#] (k,V) is non proper Element of bool the carrier of (k,V)

the carrier of (k,V) is set

bool the carrier of (k,V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

dom (center_of_mass k) is Element of bool (BOOL the carrier of k)

bool (BOOL the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

Aff is ext-real set

{} + Aff is ext-real set

{} + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

(degree V) + Aff is ext-real set

the topology of (k,V) is Element of bool (bool the carrier of (k,V))

bool (bool the carrier of (k,V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

x is set

C is finite non dependent Element of bool the carrier of (k,V)

X is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)

(center_of_mass k) .: X is finite Element of bool the carrier of k

X /\ (dom (center_of_mass k)) is finite Element of bool (BOOL the carrier of k)

(center_of_mass k) .: (X /\ (dom (center_of_mass k))) is finite Element of bool the carrier of k

F is Element of bool the carrier of V

union X is finite Element of bool the carrier of V

A1 is finite non dependent Element of bool the carrier of V

S is set

(k,V,A1) is Element of bool the carrier of k

card A1 is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

(degree V) + 1 is ext-real set

S is set

{S} is non empty trivial finite 1 -element set

{A1} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)

F is set

Im ((center_of_mass k),A1) is set

(center_of_mass k) . A1 is set

{((center_of_mass k) . A1)} is non empty trivial finite 1 -element set

CA is Element of the carrier of k

{CA} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

Sum {CA} is Element of the carrier of k

1 / 1 is non empty V21() V29() ext-real positive non negative Element of REAL

(1 / 1) * (Sum {CA}) is Element of the carrier of k

{((1 / 1) * (Sum {CA}))} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

{(Sum {CA})} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

x is set

C is finite non dependent Element of bool the carrier of V

F is Element of bool the carrier of (k,V)

{C} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)

X is Element of bool the carrier of V

A1 is set

X is finite finite-membered simplex-like Element of bool (bool the carrier of V)

S is set

card C is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

(degree V) + 1 is ext-real set

(k,V,C) is Element of bool the carrier of k

A1 is set

{A1} is non empty trivial finite 1 -element set

(center_of_mass k) .: X is finite Element of bool the carrier of k

Im ((center_of_mass k),C) is set

(center_of_mass k) . C is set

{((center_of_mass k) . C)} is non empty trivial finite 1 -element set

S is Element of the carrier of k

{S} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

Sum {S} is Element of the carrier of k

1 / 1 is non empty V21() V29() ext-real positive non negative Element of REAL

(1 / 1) * (Sum {S}) is Element of the carrier of k

{((1 / 1) * (Sum {S}))} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

{(Sum {S})} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k

F is Element of bool the carrier of (k,V)

k is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] Aff is non proper Element of bool the carrier of Aff

the carrier of Aff is set

bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

degree Aff is ext-real set

the topology of Aff is Element of bool (bool the carrier of Aff)

bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

TopStruct(# the carrier of Aff, the topology of Aff #) is strict TopStruct

(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

BOOL the carrier of V is set

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)

bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)

center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]

[:(BOOL the carrier of V), the carrier of V:] is Relation-like set

bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

dom (center_of_mass V) is Element of bool (BOOL the carrier of V)

bool (BOOL the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

(F,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

degree (F,V,Aff) is ext-real set

F + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real positive non negative finite cardinal Element of REAL

((F + 1),V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

degree ((F + 1),V,Aff) is ext-real set

subdivision ((center_of_mass V),Aff) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

degree (subdivision ((center_of_mass V),Aff)) is ext-real set

(V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

(V,(F,V,Aff)) is Element of bool the carrier of V

[#] (F,V,Aff) is non proper Element of bool the carrier of (F,V,Aff)

the carrier of (F,V,Aff) is set

bool the carrier of (F,V,Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(V,(F,V,Aff)) is non void subset-closed finite-membered non with_non-empty_elements (V,(F,V,Aff))

({},V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)

degree ({},V,Aff) is ext-real set

k is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal set

V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of V is non empty set

Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V

(V,Aff) is Element of bool the carrier of V

bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] Aff is non proper Element of bool the carrier of Aff

the carrier of Aff is set

bool the carrier of Aff is non empt