let a, b be set ; :: thesis: ( a is Subset of iff a c= b )

hereby :: thesis: ( a c= b implies a is Subset of )

assume a is Subset of ; :: thesis: a c= b
then a in bool b by SUBSET_1:def 2;
hence a c= b by ZFMISC_1:def 1; :: thesis: verum

end;

assume a c= b ; :: thesis: a is Subset of
then a in bool b by ZFMISC_1:def 1;
hence a is Subset of by SUBSET_1:def 2; :: thesis: verum