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