let V be RealLinearSpace; :: thesis:
let v be VECTOR of V; :: thesis:
let A be Subset of V; :: thesis:
set Av = A \/ {v};
v in {v} by TARSKI:def 1;
then A1: v in A \/ {v} by XBOOLE_0:def 3;
A2: A c= A \/ {v} by XBOOLE_1:7;

hereby :: thesis:

assume A3: A \/ {v} is affinely-independent ; :: thesis:
hence A is affinely-independent by Th43, XBOOLE_1:7; :: thesis:
( v in Affin A implies v in A )

proof

assume v in Affin A ; :: thesis:
then {v} c= Affin A by ZFMISC_1:31;
then Affin (A \/ {v}) = Affin A by Th69;
hence v in A by A2, A1, A3, Th58; :: thesis:

end;

hence ( v in A or not v in Affin A ) ; :: thesis:

end;

assume that
A4: A is affinely-independent and
A5: ( v in A or not v in Affin A ) ; :: thesis:

per cases by A5;

suppose v in A ; :: thesis:

hence A \/ {v} is affinely-independent by A4, ZFMISC_1:40; :: thesis:

end;

suppose A6: ( not v in Affin A & not v in A ) ; :: thesis:

consider I being affinely-independent Subset of V such that
A7: A c= I and
A8: I c= A \/ {v} and
A9: Affin I = Affin (A \/ {v}) by A2, A4, Th60;
assume A10: not A \/ {v} is affinely-independent ; :: thesis:
not v in I

proof

assume v in I ; :: thesis:
then {v} c= I by ZFMISC_1:31;
hence contradiction by A7, A10, Th43, XBOOLE_1:8; :: thesis:

end;

then A11: I c= (A \/ {v}) \ {v} by A8, ZFMISC_1:34;
A12: A \/ {v} c= Affin (A \/ {v}) by Lm7;
(A \/ {v}) \ {v} = A by A6, ZFMISC_1:117;
then I = A by A7, A11;
hence contradiction by A1, A6, A9, A12; :: thesis:

end;

end;