set x = {1};
take {1} ; :: thesis: ( not {1} is empty & {1} is with_finite-elements )
thus not {1} is empty ; :: thesis: {1} is with_finite-elements
for y being Element of {1} holds y is finite ;
hence {1} is with_finite-elements by Def1; :: thesis: verum