theorem :: SCMFSA6A:16

for I, J being Program of holds Directed I c= I ";" J