:: deftheorem defines Obs QMAX_1:def 2 :
for Q being QM_Str holds Obs Q = the Observables of Q;