let X be set ; :: thesis: for x being object st x in X & card X = 1 holds

{x} = X

let x be object ; :: thesis: ( x in X & card X = 1 implies {x} = X )

assume that

A1: x in X and

A2: card X = 1 ; :: thesis: {x} = X

consider y being object such that

B1: X = {y} by CARD_2:42, A2;

x in {y} by B1, A1;

then x = y by TARSKI:def 1;

hence {x} = X by B1; :: thesis: verum

{x} = X

let x be object ; :: thesis: ( x in X & card X = 1 implies {x} = X )

assume that

A1: x in X and

A2: card X = 1 ; :: thesis: {x} = X

consider y being object such that

B1: X = {y} by CARD_2:42, A2;

x in {y} by B1, A1;

then x = y by TARSKI:def 1;

hence {x} = X by B1; :: thesis: verum