theorem Th30: :: ARMSTRNG:30

for X being finite set
for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F