take x = {{{}}}; :: thesis: ( not x is empty & x is finite & x is finite-membered )
thus ( not x is empty & x is finite ) ; :: thesis: x is finite-membered
let y be set ; :: according to FINSET_1:def 6 :: thesis: ( y in x implies y is finite )
thus ( y in x implies y is finite ) by TARSKI:def 1; :: thesis: verum