theorem :: ARMSTRNG:25

for X being set
for F being Dependency-set of X holds Maximal_wrt F c= F ;