:: deftheorem defines ";" SCMFSA6A:def 3 :
for I, J being Program of holds I ";" J = (stop (Directed I)) ';' J;