let X, A, B be set ; :: thesis: ( A in Fin X & B c= A implies B in Fin X )
assume that
A1: A in Fin X and
A2: B c= A ; :: thesis: B in Fin X
( A is finite & A c= X ) by A1, FINSUB_1:def 5;
then ( B is finite & B c= X ) by A2, XBOOLE_1:1;
hence B in Fin X by FINSUB_1:def 5; :: thesis: verum