let X, Y be set ; :: thesis: ( ( for x being set st x in X holds
x in Y ) implies X is Subset of Y )
assume for x being set st x in X holds
x in Y ; :: thesis: X is Subset of Y
then X c= Y by TARSKI:def 3;
then X in bool Y by ZFMISC_1:def 1;
hence X is Subset of Y by Def2; :: thesis: verum