consider O, A being empty set ;
( 2-sorted(# O,A #) is empty & 2-sorted(# O,A #) is void & 2-sorted(# O,A #) 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