defpred S₁[] means for x being set st x is X,D -provable holds
x in X;
thus ( X is D -expanded implies S₁[] ) :: thesis: ( ( for x being set st x is X,D -provable holds
x in X ) implies X is D -expanded )

proof

assume B1: X is D -expanded ; :: thesis: S₁[]

hereby :: thesis: verum

let x be set ; :: thesis: ( x is X,D -provable implies x in X )
assume x is X,D -provable ; :: thesis: x in X
then {x} c= X by B1, DefExpanded;
hence x in X by ZFMISC_1:31; :: thesis: verum

end;

end;

assume B0: S₁[] ; :: thesis: X is D -expanded

hereby :: according to FOMODEL4:def 16 :: thesis: verum

let x be set ; :: thesis: ( x is X,D -provable implies {x} c= X )
assume x is X,D -provable ; :: thesis: {x} c= X
then x in X by B0;
hence {x} c= X by ZFMISC_1:31; :: thesis: verum

end;