theorem :: SCMFSA6A:36

for I being preProgram of SCM+FSA holds card (Directed I) = card I by Lm1;