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