let X be set ; :: thesis: ( X is axiom_GU2 implies for x being set st x in X holds
{x} in X )
assume A1: X is axiom_GU2 ; :: thesis: for x being set st x in X holds
{x} in X
let x be set ; :: thesis: ( x in X implies {x} in X )
assume A2: x in X ; :: thesis: {x} in X
{x} = {x,x} by ENUMSET1:29;
hence {x} in X by A1, A2; :: thesis: verum