theorem :: SUBSET_1:19

for E being set
for A being Subset of E holds
( A ` c= A iff A = [#] E )