theorem Th27: :: SF_MASTR:27

for I, J being Program of holds UsedILoc (I ";" J) = (UsedILoc I) \/ (UsedILoc J)