theorem Th1: :: YELLOW_8:1

for X, A, B being set st A in Fin X & B c= A holds
B in Fin X