{the Element of S} is Subset of S by ZFMISC_1:37;
hence ex b₁ being Subset of S st
( not b₁ is empty & b₁ is trivial ) ; :: thesis: verum