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

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

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

end;

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