Example is MidSp-like by Def4, Th10;
hence ex b₁ being non empty MidStr st
( b₁ is strict & b₁ is MidSp-like ) ; :: thesis: verum