theorem :: ARMSTRNG:46

for X being non empty finite set
for F being Full-family of X ex R being DB-Rel st
( the Attributes of R = X & ( for a being Element of X holds the Domains of R . a = INT ) & F = Dependency-str R )