theorem :: ARMSTRNG:58

for X being non empty finite set
for F, G being Dependency-set of X st charact_set F = charact_set G holds
Dependency-closure F = Dependency-closure G