consider S being non empty non void strict ManySortedSign ;
set A = {S};
for x being set st x in {S} holds
x is non empty non void strict ManySortedSign by TARSKI:def 1;
then {S} is MSS-membered by Def7;
hence ex b₁ being set st
( not b₁ is empty & b₁ is MSS-membered ) ; :: thesis: verum