let X be set ; :: thesis: for x being object st x in X holds
Class ((id X),x) = {x}
let x be object ; :: thesis: ( x in X implies Class ((id X),x) = {x} )

A1: now :: thesis: for y being object st y in Class ((id X),x) holds
y = x

let y be object ; :: 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 Th19;
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 object holds
( y in Class ((id X),x) iff y = x ) by A1, Th20;
hence Class ((id X),x) = {x} by TARSKI:def 1; :: thesis: verum