theorem :: ARMSTRNG:56

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