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