:: deftheorem defines is_a_coordinate BVFUNC_2:def 6 :
for Y being non empty set
for G being Subset of (PARTITIONS Y) holds
( G is_a_coordinate iff ( G is independent & G is generating ) );