consider O being non empty set ;
consider M being non empty calculating_type halting Moore-SM_Final of I,O;
take M ; :: thesis: ( M is calculating_type & M is halting )
thus ( M is calculating_type & M is halting ) ; :: thesis: verum