:: deftheorem defines Prop QMAX_1:def 8 :
for Q being Quantum_Mechanics holds Prop Q = [:(Obs Q),Borel_Sets:];