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