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} )

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

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

assume
x in X
; :: thesis: Class ((id X),x) = {x}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 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

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