theorem :: ARMSTRNG:20

for X being finite set
for F being Dependency-set of X holds F is finite ;