let F be Subset-Family of V; :: thesis: ( F is empty implies F is affinely-independent )
assume A1: F is empty ; :: thesis: F is affinely-independent
let A be Subset of V; :: according to RLAFFIN1:def 5 :: thesis: ( A in F implies A is affinely-independent )
assume A in F ; :: thesis: A is affinely-independent
hence A is affinely-independent by A1; :: thesis: verum