:: deftheorem defines is_p_i_w_ncv_of ARMSTRNG:def 32 :
for A, K being set
for F being Dependency-set of A holds
( K is_p_i_w_ncv_of F iff ( ( for a being Subset of A st K c= a & a <> A holds
a in charact_set F ) & ( for k being set st k c< K holds
ex a being Subset of A st
( k c= a & a <> A & not a in charact_set F ) ) ) );