let X be set ; :: thesis: for x being object st x in X holds
Class ((nabla X),x) = X
let x be object ; :: thesis: ( x in X implies Class ((nabla X),x) = X )
assume A1: x in X ; :: thesis: Class ((nabla X),x) = X

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

let y be object ; :: thesis: ( y in X implies y in Class ((nabla X),x) )
assume y in X ; :: thesis: y in Class ((nabla X),x)
then [y,x] in nabla X by A1, ZFMISC_1:87;
hence y in Class ((nabla X),x) by Th19; :: thesis: verum

end;

then for y being object holds
( y in X iff y in Class ((nabla X),x) ) ;
hence Class ((nabla X),x) = X by TARSKI:2; :: thesis: verum