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