let V be RealLinearSpace; :: thesis: for A, B being finite Subset of V st A is affinely-independent & Affin A = Affin B & card B <= card A holds
B is affinely-independent
let A, B be finite Subset of V; :: thesis: ( A is affinely-independent & Affin A = Affin B & card B <= card A implies B is affinely-independent )
assume that
A1: A is affinely-independent and
A2: Affin A = Affin B and
A3: card B <= card A ; :: thesis: B is affinely-independent

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: B is affinely-independent

then B is empty by A3, XXREAL_0:1;
hence B is affinely-independent ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: B is affinely-independent

then consider p being object such that
A4: p in A ;
card A > 0 by A4;
then reconsider n = (card A) - 1 as Element of NAT by NAT_1:20;
A5: A c= Affin A by Lm7;
reconsider p = p as Element of V by A4;
set L = Lin ((- p) + A);
{} V c= B ;
then consider Ia being affinely-independent Subset of V such that
{} V c= Ia and
A6: Ia c= B and
A7: Affin Ia = Affin B by Th60;
not Ia is empty by A2, A4, A7;
then consider q being object such that
A8: q in Ia ;
(- p) + A c= [#] (Lin ((- p) + A))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- p) + A or x in [#] (Lin ((- p) + A)) )
assume x in (- p) + A ; :: thesis: x in [#] (Lin ((- p) + A))
then x in Lin ((- p) + A) by RLVECT_3:15;
hence x in [#] (Lin ((- p) + A)) ; :: thesis: verum

end;

then reconsider pA = (- p) + A as Subset of (Lin ((- p) + A)) ;
((- p) + A) \ {(0. V)} is linearly-independent by A1, A4, Th41;
then A9: pA \ {(0. V)} is linearly-independent by RLVECT_5:15;
(- p) + p = 0. V by RLVECT_1:5;
then A10: 0. V in pA by A4;
then Lin ((- p) + A) = Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116
.= Lin (((- p) + A) \ {(0. V)}) by Lm9
.= Lin (pA \ {(0. V)}) by RLVECT_5:20 ;
then A11: pA \ {(0. V)} is Basis of Lin ((- p) + A) by A9, RLVECT_3:def 3;
reconsider IA = Ia as finite set by A6;
A12: Ia c= Affin Ia by Lm7;
reconsider q = q as Element of V by A8;
p + (Lin ((- p) + A)) = p + (Up (Lin ((- p) + A))) by RUSUB_4:30
.= Affin A by A4, A5, Th57
.= q + (Up (Lin ((- q) + Ia))) by A2, A7, A8, A12, Th57
.= q + (Lin ((- q) + Ia)) by RUSUB_4:30 ;
then A13: Lin ((- p) + A) = Lin ((- q) + Ia) by RLSUB_1:69;
set qI = (- q) + Ia;
A14: (- q) + Ia c= [#] (Lin ((- q) + Ia))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- q) + Ia or x in [#] (Lin ((- q) + Ia)) )
assume x in (- q) + Ia ; :: thesis: x in [#] (Lin ((- q) + Ia))
then x in Lin ((- q) + Ia) by RLVECT_3:15;
hence x in [#] (Lin ((- q) + Ia)) ; :: thesis: verum

end;

card pA = n + 1 by Th7;
then A15: card (pA \ {(0. V)}) = n by A10, STIRL2_1:55;
then pA \ {(0. V)} is finite ;
then A16: Lin ((- p) + A) is finite-dimensional by A11, RLVECT_5:def 1;
reconsider qI = (- q) + Ia as Subset of (Lin ((- q) + Ia)) by A14;
((- q) + Ia) \ {(0. V)} is linearly-independent by A8, Th41;
then A17: qI \ {(0. V)} is linearly-independent by RLVECT_5:15;
(- q) + q = 0. V by RLVECT_1:5;
then A18: 0. V in qI by A8;
then Lin ((- q) + Ia) = Lin ((((- q) + Ia) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116
.= Lin (((- q) + Ia) \ {(0. V)}) by Lm9
.= Lin (qI \ {(0. V)}) by RLVECT_5:20 ;
then qI \ {(0. V)} is Basis of Lin ((- q) + Ia) by A17, RLVECT_3:def 3;
then A19: card (qI \ {(0. V)}) = n by A11, A13, A15, A16, RLVECT_5:25;
then ( not 0. V in qI \ {(0. V)} & qI \ {(0. V)} is finite ) by ZFMISC_1:56;
then A20: n + 1 = card ((qI \ {(0. V)}) \/ {(0. V)}) by A19, CARD_2:41
.= card qI by A18, ZFMISC_1:116
.= card Ia by Th7 ;
card IA <= card B by A6, NAT_1:43;
hence B is affinely-independent by A3, A6, A20, CARD_2:102, XXREAL_0:1; :: thesis: verum

end;

end;