let V be RealLinearSpace; :: thesis: for A, B being Subset of V st A is affinely-independent & B c= A holds

B is affinely-independent

let A, B be Subset of V; :: thesis: ( A is affinely-independent & B c= A implies B is affinely-independent )

assume that

A1: A is affinely-independent and

A2: B c= A ; :: thesis: B is affinely-independent

B is affinely-independent

let A, B be Subset of V; :: thesis: ( A is affinely-independent & B c= A implies B is affinely-independent )

assume that

A1: A is affinely-independent and

A2: B c= A ; :: thesis: B is affinely-independent

now :: thesis: for L being Linear_Combination of B st Sum L = 0. V & sum L = 0 holds

Carrier L = {}

hence
B is affinely-independent
by Th42; :: thesis: verumCarrier L = {}

let L be Linear_Combination of B; :: thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )

assume A3: ( Sum L = 0. V & sum L = 0 ) ; :: thesis: Carrier L = {}

L is Linear_Combination of A by A2, RLVECT_2:21;

hence Carrier L = {} by A1, A3, Th42; :: thesis: verum

end;assume A3: ( Sum L = 0. V & sum L = 0 ) ; :: thesis: Carrier L = {}

L is Linear_Combination of A by A2, RLVECT_2:21;

hence Carrier L = {} by A1, A3, Th42; :: thesis: verum