begin
Lm1:
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
Lm3:
for S being non empty addLoopStr
for v, w being Element of S holds {(v + w)} = v + {w}
Lm4:
for V being non empty addLoopStr
for A being Subset of V
for v being Element of V holds card (v + A) c= card A
begin
begin
begin
Lm5:
for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
Lm6:
for V being RealLinearSpace
for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) holds
for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
begin
Lm7:
for V being non empty RLSStruct
for A being Subset of V holds A c= Affin A
Lm8:
for V being non empty RLSStruct
for A being Affine Subset of V holds A = Affin A
Lm9:
for V being RealLinearSpace
for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
begin