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