( weight T1 c= omega & weight T2 c= omega ) by WAYBEL23:def 6;
then A1: (weight T1) *` (weight T2) c= omega by CARD_2:90, CARD_4:6;
weight [:T1,T2:] c= (weight T1) *` (weight T2) by Th5;
then weight [:T1,T2:] c= omega by A1;
hence [:T1,T2:] is second-countable by WAYBEL23:def 6; :: thesis: verum