theorem Th27: :: SCMFSA6A:37

for I being Program of holds card (stop (Directed I)) = card (stop I) by Lm2;