defpred S1[] means for x being set st x is X,D -provable holds
x in X;
thus ( X is D -expanded implies S1[] ) :: 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: S1[]
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: S1[] ; :: 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