set O = the non empty set ;
set M = the non empty calculating_type halting Moore-SM_Final over I, the non empty set ;
take the non empty calculating_type halting Moore-SM_Final over I, the non empty set ; :: thesis: ( the non empty calculating_type halting Moore-SM_Final over I, the non empty set is calculating_type & the non empty calculating_type halting Moore-SM_Final over I, the non empty set is halting )
thus ( the non empty calculating_type halting Moore-SM_Final over I, the non empty set is calculating_type & the non empty calculating_type halting Moore-SM_Final over I, the non empty set is halting ) ; :: thesis: verum