theorem Th18: :: ARMSTRNG:18

for X being set
for F being Dependency-set of X holds
( F is (F2) iff for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F )