theorem Th55: :: ARMSTRNG:55

for X, A being set
for F being Dependency-set of X st A in charact_set F holds
( A is Subset of X & ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) )