( X c= I & Y c= J ) by FINSUB_1:def 5;
then [:X,Y:] c= [:I,J:] by ZFMISC_1:96;
hence [:X,Y:] is Element of Fin [:I,J:] by FINSUB_1:def 5; :: thesis: verum