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 A1: 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 A1;
hence x in X by ZFMISC_1:31; :: thesis: verum

end;

end;

assume A2: S₁[] ; :: thesis: X is D -expanded
thus for x being set st x is X,D -provable holds
{x} c= X by ZFMISC_1:31, A2; :: according to FOMODEL4:def 17 :: thesis: verum