not 2-sorted(# {{} },{{} } #) is quasi-empty by Def2;
hence ex b₁ being 2-sorted st
( b₁ is strict & not b₁ is quasi-empty ) ; :: thesis: verum