QM_Str(# X,X,Y #) is Quantum_Mechanics-like by Def5, Lm8;
hence ex b₁ being QM_Str st
( b₁ is strict & b₁ is Quantum_Mechanics-like ) ; :: thesis: verum