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