take Stop S ; :: thesis: ( Stop S is initial & Stop S is NAT -defined & not Stop S is empty )
thus ( Stop S is initial & Stop S is NAT -defined & not Stop S is empty ) ; :: thesis: verum