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