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
thus x is with_finite-elements ; :: thesis: verum