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

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