take X = {1}; :: thesis: ( X is finite & not X is empty & X is natural-membered & X is with_non-empty_elements )
thus ( X is finite & not X is empty ) ; :: thesis: ( X is natural-membered & X is with_non-empty_elements )
thus X is natural-membered ; :: thesis: X is with_non-empty_elements
thus X is with_non-empty_elements ; :: thesis: verum