:: deftheorem Def24 defines Dependency-closure ARMSTRNG:def 24 :
for X being non empty finite set
for F being Dependency-set of X
for b₃ being Full-family of X holds
( b₃ = Dependency-closure F iff ( F c= b₃ & ( for G being Dependency-set of X st F c= G & G is full_family holds
b₃ c= G ) ) );