environ
vocabularies HIDDEN, ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CARD_2, CLASSES1, COHSP_1, COMPLEX1, CONVEX1, CONVEX2, CONVEX3, FINSEQ_1, FINSET_1, FUNCT_1, MATROID0, MCART_1, ORDERS_1, PARTFUN1, PRE_TOPC, QC_LANG1, RELAT_1, RLVECT_1, RLVECT_2, SEMI_AF1, SETFAM_1, SGRAPH1, SUBSET_1, TARSKI, TOPS_1, ZFMISC_1, RLAFFIN1, RLAFFIN2, SIMPLEX0, SIMPLEX1, REAL_1, FUNCOP_1, NAT_1, FUNCT_2, STRUCT_0, XXREAL_0, NUMBERS, ORDINAL1, CARD_3, GLIB_000, FINSEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XXREAL_3, XXREAL_0, XCMPLX_0, XREAL_0, ORDERS_1, CARD_1, REAL_1, FINSET_1, WELLORD2, SETFAM_1, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, FINSEQ_1, STRUCT_0, CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2, CONVEX1, CONVEX2, CONVEX3, PRE_TOPC, RLAFFIN1, FUNCOP_1, PENCIL_1, MATROID0, XTUPLE_0, MCART_1, CARD_2, COHSP_1, SIMPLEX0, RLAFFIN2;
definitions ORDINAL1, SETFAM_1, TARSKI, TOPS_2, XBOOLE_0, FINSET_1;
theorems CARD_1, CARD_2, CLASSES1, COHSP_1, CONVEX1, CONVEX3, FINSEQ_1, FINSEQ_3, FUNCOP_1, FUNCT_1, FUNCT_2, INT_1, MATROID0, MCART_1, NAT_1, ORDINAL1, PENCIL_1, PRE_TOPC, RELAT_1, RELSET_2, RLTOPSP1, RLVECT_1, RLVECT_2, RVSUM_1, STIRL2_1, TARSKI, TOPS_2, WELLORD2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_3, ZFMISC_1, RLAFFIN1, RLAFFIN2, SIMPLEX0, XTUPLE_0;
schemes CLASSES1, FUNCT_1, FUNCT_2, NAT_1, RELAT_1;
registrations CARD_1, FINSET_1, FUNCT_1, NAT_1, RELAT_1, RLVECT_1, STRUCT_0, SUBSET_1, VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, XBOOLE_0, RLAFFIN1, SIMPLEX0, FUNCOP_1, INT_1, XXREAL_3, MATROID0, SETFAM_1, COHSP_1, RLAFFIN2, RELSET_1, RLVECT_2, ORDINAL1, XTUPLE_0, FINSEQ_1;
constructors HIDDEN, BINOP_2, CONVEX1, CONVEX3, REAL_1, RVSUM_1, RLAFFIN1, SIMPLEX0, TOPS_2, BORSUK_1, COHSP_1, CARD_2, RLAFFIN2, XTUPLE_0;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities MATROID0, ORDERS_1, RLVECT_2, STRUCT_0, SIMPLEX0, XXREAL_3, CARD_1, ORDINAL1;
expansions MATROID0, ORDINAL1, SETFAM_1, SIMPLEX0, TARSKI, TOPS_2, XBOOLE_0;
Lm1:
for V being RealLinearSpace
for S being finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})