take F = Stop S; :: thesis: ( F is really-closed & F is trivial )
thus ( F is really-closed & F is trivial ) ; :: thesis: verum