let X, x be set ; :: thesis: ( x in X implies Class (id X),x = {x} )

A1: now

let y be set ; :: thesis: ( y in Class (id X),x implies y = x )
assume y in Class (id X),x ; :: thesis: y = x
then [y,x] in id X by Th27;
hence y = x by RELAT_1:def 10; :: thesis: verum

end;

assume x in X ; :: thesis: Class (id X),x = {x}
then for y being set holds
( y in Class (id X),x iff y = x ) by A1, Th28;
hence Class (id X),x = {x} by TARSKI:def 1; :: thesis: verum