let D be finite set ; :: thesis: ( card D = 1 implies ex x being Element of D st D = {x} )
assume card D = 1 ; :: thesis: ex x being Element of D st D = {x}
then card D = 0 + 1 ;
then consider x being Element of D, C being Subset of D such that
A1: D = C \/ {x} and
A2: card C = 0 by Th23;
take x ; :: thesis: D = {x}
C = {} by A2;
hence D = {x} by A1; :: thesis: verum