take F = Stop S; :: thesis: ( F is halt-ending & F is unique-halt & F is trivial )
thus ( F is halt-ending & F is unique-halt & F is trivial ) ; :: thesis: verum