set SA = Start-At (0,SCM+FSA);
let I be Program of SCM+FSA; :: thesis: ( I is paraclosed implies I is InitClosed )
assume A1: I is paraclosed ; :: thesis: I is InitClosed
A2: I +* (Start-At (0,SCM+FSA)) c= Initialized I by Th6;
for s being State of SCM+FSA
for n being Element of NAT st Initialized I c= s holds
IC (Comput ((ProgramPart s),s,n)) in dom I by A1, A2, SCMFSA6B:def 2, XBOOLE_1:1;
hence I is InitClosed by Def1; :: thesis: verum