theorem :: SUBSET_1:28

for E being set
for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A