take halt SCM+FSA ; :: thesis: ( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting )
thus ( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting ) ; :: thesis: verum