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