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 c= X by A1, FINSUB_1:def 5;
then B c= X by A2;
hence B in Fin X by A1, A2, FINSUB_1:def 5; :: thesis: verum