let s be State of ; :: thesis: for I being paraclosed Program of holds insloc 0 in dom I
let I be paraclosed Program of ; :: thesis: insloc 0 in dom I
I is_closed_on s by SCMFSA7B:24;
hence insloc 0 in dom I by Th39; :: thesis: verum