theorem :: SUBSET:5

for a, b, c being set st a in b & b is Subset of c holds
not c is empty ;