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

end;

suppose
v = w
; :: thesis: for b_{1} being Subset of V st b_{1} = {v,w} holds

b_{1} is affinely-independent

b

then
{v,w} = {w}
by ENUMSET1:29;

hence for b_{1} being Subset of V st b_{1} = {v,w} holds

b_{1} is affinely-independent
; :: thesis: verum

end;hence for b

b

suppose A1:
v <> w
; :: thesis: for b_{1} being Subset of V st b_{1} = {v,w} holds

b_{1} is affinely-independent

b

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

- (- 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_{1} being Subset of V st b_{1} = {v,w} holds

b_{1} is affinely-independent
; :: thesis: verum

end;proof

then A4:
((- v) + {v,w}) \ {(0. V)} c= {((- v) + w),(0. V)} \ {(0. V)}
by XBOOLE_1:33;
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} ;

end;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} ;

- (- 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

hence
for b
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;( 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

b