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

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