theorem :: SCMFSA6A:38

for I, J being Program of holds Reloc (J,(card I)) c= I ";" J