take X = {{}}; :: thesis: ( not X is empty & X is FinSequence-membered )
thus ( not X is empty & X is FinSequence-membered ) ; :: thesis: verum