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