let V be RealLinearSpace; :: thesis: for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent

let I be Basis of V; :: thesis: for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent

let A be non empty Subset of V; :: thesis: ( A misses I implies for B being Subset of V st B = I \/ A holds
B is linearly-dependent )

assume A1: A misses I ; :: thesis: for B being Subset of V st B = I \/ A holds
B is linearly-dependent

consider v being object such that
A2: v in A by XBOOLE_0:def 1;
let B be Subset of V; :: thesis: ( B = I \/ A implies B is linearly-dependent )
assume A3: B = I \/ A ; :: thesis:
A4: A c= B by ;
reconsider v = v as VECTOR of V by A2;
reconsider Bv = B \ {v} as Subset of V ;
A5: I \ {v} c= B \ {v} by ;
not v in I by ;
then I c= Bv by ;
then A6: Lin I is Subspace of Lin Bv by RLVECT_3:20;
assume A7: B is linearly-independent ; :: thesis: contradiction
v in Lin I by Th13;
hence contradiction by A7, A2, A4, A6, Th17, RLSUB_1:8; :: thesis: verum