let X, x be set ; :: thesis: ( x in X implies Class ((nabla X),x) = X )
assume A1: x in X ; :: thesis: Class ((nabla X),x) = X

now

let y be set ; :: 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:106;
hence y in Class ((nabla X),x) by Th27; :: thesis: verum

end;

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