set XX = _bool A;
semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) by Def6;
hence ( not _bool A is empty & _bool A is deterministic ) by Def5; :: thesis: verum