consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:74;
B | A is Basis of (T | A) by Th8;
then A2: weight (T | A) c= card (B | A) by WAYBEL23:73;
card (B | A) c= card B by Th7;
then ( weight T c= omega & weight (T | A) c= weight T ) by A1, A2, WAYBEL23:def 6;
then weight (T | A) c= omega ;
hence T | A is second-countable by WAYBEL23:def 6; :: thesis: verum