theorem Th9: :: ARMSTRNG:9

for X, x being set
for F being Dependency-set of X st x in F holds
ex a, b being Subset of X st x = [a,b]