theorem :: SUBSET:1

for a, b being set st a in b holds
a is Element of b by SUBSET_1:def 1;