let V be RealLinearSpace; :: thesis: for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B & card A = card B holds

B is affinely-independent

let A, B be finite Subset of V; :: thesis: ( A is affinely-independent & Affin A c= Affin B & card A = card B implies B is affinely-independent )

assume A1: ( A is affinely-independent & Affin A c= Affin B & card A = card B ) ; :: thesis: B is affinely-independent

{} V c= B ;

then consider Ib being affinely-independent Subset of V such that

{} V c= Ib and

A2: Ib c= B and

A3: Affin Ib = Affin B by Th60;

reconsider IB = Ib as finite Subset of V by A2;

A4: card IB <= card B by A3, Th79;

card B <= card IB by A1, A3, Th79;

hence B is affinely-independent by A2, A4, CARD_2:102, XXREAL_0:1; :: thesis: verum

B is affinely-independent

let A, B be finite Subset of V; :: thesis: ( A is affinely-independent & Affin A c= Affin B & card A = card B implies B is affinely-independent )

assume A1: ( A is affinely-independent & Affin A c= Affin B & card A = card B ) ; :: thesis: B is affinely-independent

{} V c= B ;

then consider Ib being affinely-independent Subset of V such that

{} V c= Ib and

A2: Ib c= B and

A3: Affin Ib = Affin B by Th60;

reconsider IB = Ib as finite Subset of V by A2;

A4: card IB <= card B by A3, Th79;

card B <= card IB by A1, A3, Th79;

hence B is affinely-independent by A2, A4, CARD_2:102, XXREAL_0:1; :: thesis: verum