theorem Th29: :: ARMSTRNG:29

for X being finite set
for M, F being Dependency-set of X st M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } holds
( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )