take Stop S ; :: thesis: ( not Stop S is halt-free & Stop S is finite )
thus ( not Stop S is halt-free & Stop S is finite ) ; :: thesis: verum