:: deftheorem defines Sts QMAX_1:def 3 :
for Q being QM_Str holds Sts Q = the FStates of Q;