for X being non empty finite set
for F being Dependency-set of X holds
( F c= X deps_encl_by (enclosure_of F) & ( for G being Dependency-set of X st F c= G & G is full_family holds
X deps_encl_by (enclosure_of F) c= G ) )