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