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

then a in bool b by ZFMISC_1:def 1;

hence a is Subset of b by SUBSET_1:def 1; :: thesis: verum

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

assume
a c= b
; :: thesis: a is Subset of bassume
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;then a in bool b by SUBSET_1:def 1;

hence a c= b by ZFMISC_1:def 1; :: thesis: verum

then a in bool b by ZFMISC_1:def 1;

hence a is Subset of b by SUBSET_1:def 1; :: thesis: verum