per cases ( v = w or v <> w ) ;

suppose v = w ; :: thesis: for b₁ being Subset of V st b₁ = {v,w} holds
b₁ is affinely-independent

then {v,w} = {w} by ENUMSET1:29;
hence for b₁ being Subset of V st b₁ = {v,w} holds
b₁ is affinely-independent ; :: thesis: verum

end;

suppose A1: v <> w ; :: thesis: for b₁ being Subset of V st b₁ = {v,w} holds
b₁ is affinely-independent

(- v) + {v,w} c= {((- v) + w),(0. V)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- v) + {v,w} or x in {((- v) + w),(0. V)} )
assume x in (- v) + {v,w} ; :: thesis: x in {((- v) + w),(0. V)}
then consider r being Element of V such that
A2: x = (- v) + r and
A3: r in {v,w} ;

per cases ( r = v or r = w ) by A3, TARSKI:def 2;

suppose r = v ; :: thesis: x in {((- v) + w),(0. V)}

then x = 0. V by A2, RLVECT_1:5;
hence x in {((- v) + w),(0. V)} by TARSKI:def 2; :: thesis: verum

end;

suppose r = w ; :: thesis: x in {((- v) + w),(0. V)}

hence x in {((- v) + w),(0. V)} by A2, TARSKI:def 2; :: thesis: verum

end;

end;

end;

then A4: ((- v) + {v,w}) \ {(0. V)} c= {((- v) + w),(0. V)} \ {(0. V)} by XBOOLE_1:33;
- (- v) = v ;
then A5: w + (- v) <> 0. V by A1, RLVECT_1:6;
then A6: {((- v) + w)} is linearly-independent by RLVECT_3:8;
{v,w} is affinely-independent

proof

assume not {v,w} is empty ; :: according to RLAFFIN1:def 4 :: thesis: ex v being VECTOR of V st
( v in {v,w} & ((- v) + {v,w}) \ {(0. V)} is linearly-independent )
take v ; :: thesis: ( v in {v,w} & ((- v) + {v,w}) \ {(0. V)} is linearly-independent )
thus v in {v,w} by TARSKI:def 2; :: thesis: ((- v) + {v,w}) \ {(0. V)} is linearly-independent
( 0. V in {(0. V)} & not (- v) + w in {(0. V)} ) by A5, TARSKI:def 1;
then ((- v) + {v,w}) \ {(0. V)} c= {((- v) + w)} by A4, ZFMISC_1:62;
hence ((- v) + {v,w}) \ {(0. V)} is linearly-independent by A6, RLVECT_3:5; :: thesis: verum

end;

hence for b₁ being Subset of V st b₁ = {v,w} holds
b₁ is affinely-independent ; :: thesis: verum

end;

end;