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