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