set Al3 = Al1 \/ Al2;
( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;
then A1: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;
NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by XBOOLE_1:10, QC_LANG1:3;
then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A1, QC_LANG1:def 1;
take Al3 ; :: thesis: ( Al3 is countable & Al3 is Al1 -expanding & Al3 is Al2 -expanding )
thus ( Al3 is countable & Al3 is Al1 -expanding & Al3 is Al2 -expanding ) by CARD_2:85, XBOOLE_1:7; :: thesis: verum