set x = {{1}};
reconsider x = {{1}} as Subset of (bool NAT) ;
take x ; :: thesis: ( not x is empty & x is finite & x is with_finite-elements )
thus not x is empty ; :: thesis: ( x is finite & x is with_finite-elements )
thus x is finite ; :: thesis: x is with_finite-elements
for y being Element of x holds y is finite by TARSKI:def 1;
hence x is with_finite-elements by Def1; :: thesis: verum