reconsider CLS = CLS as CollSp by Lm8;
CLS is proper by Lm7;
hence ex b₁ being CollSp st
( b₁ is strict & b₁ is proper ) ; :: thesis: verum