let V be RealLinearSpace; :: thesis: for F1, F2 being Subset-Family of V st F1 c= F2 & F2 is affinely-independent holds
F1 is affinely-independent
let F1, F2 be Subset-Family of V; :: thesis: ( F1 c= F2 & F2 is affinely-independent implies F1 is affinely-independent )
assume A1: ( F1 c= F2 & F2 is affinely-independent ) ; :: thesis: F1 is affinely-independent
let A be Subset of V; :: according to RLAFFIN1:def 5 :: thesis: ( A in F1 implies A is affinely-independent )
assume A in F1 ; :: thesis: A is affinely-independent
hence A is affinely-independent by A1, Def5; :: thesis: verum