( a in Bags I & b in Bags I ) by PRE_POLY:def 12;
hence [a,b] is Element of [:(Bags I),(Bags I):] by ZFMISC_1:87; :: thesis: verum