set TS = _bool SA;
the InitS of (_bool SA) = {((<%> E) -succ_of ( the InitS of SA,SA))}
by Def3;
then A1:
card the InitS of (_bool SA) = 1
by CARD_1:30;
transition-system(# the carrier of (_bool SA), the Tran of (_bool SA) #) = _bool transition-system(# the carrier of SA, the Tran of SA #)
by Def3;
hence
( not _bool SA is empty & _bool SA is deterministic )
by A1; verum