take Stop SCM+FSA ; :: thesis: ( Stop SCM+FSA is keepInt0_1 & Stop SCM+FSA is InitHalting )
thus ( Stop SCM+FSA is keepInt0_1 & Stop SCM+FSA is InitHalting ) ; :: thesis: verum