theorem Th12: :: ARMSTRNG:12

for X being set
for P, Q, S being Dependency of X st P <= Q & Q <= S holds
P <= S