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
now :: thesis: for L being Linear_Combination of B st Sum L = 0. V & sum L = 0 holds
Carrier 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;
hence B is affinely-independent by Th42; :: thesis: verum