let I be Program of SCM+FSA; :: thesis: ( I is InitClosed iff for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_on Initialized s,p )

hereby :: thesis: ( ( for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_on Initialized s,p ) implies I is InitClosed )

assume A1: I is InitClosed ; :: thesis: for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_on Initialized s,p
let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA holds I is_closed_on Initialized s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: I is_closed_on Initialized s,p
I is_closed_onInit s,p by A1, Th35;
hence I is_closed_on Initialized s,p by Th40; :: thesis: verum

end;

assume A2: for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_on Initialized s,p ; :: thesis: I is InitClosed

now

let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: I is_closed_onInit s,p
I is_closed_on Initialized s,p by A2;
hence I is_closed_onInit s,p by Th40; :: thesis: verum

end;

hence I is InitClosed by Th35; :: thesis: verum