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