let A be QC-alphabet ; :: thesis: for x being set holds
( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) )
let x be set ; :: thesis: ( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) )
thus ( not x in QC-variables A or x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) :: thesis: ( ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) implies x in QC-variables A )

proof

assume x in QC-variables A ; :: thesis: ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A )
then x in [:{6},NAT:] \/ [:{4,5},(QC-symbols A):] by QC_LANG1:def 3;
then ( x in [:{6},NAT:] or x in [:{4,5},(QC-symbols A):] ) by XBOOLE_0:def 3;
then consider x1, x2 being object such that
A1: ( ( x1 in {6} & x2 in NAT & x = [x1,x2] ) or ( x1 in {4,5} & x2 in QC-symbols A & x = [x1,x2] ) ) by ZFMISC_1:def 2;
( ( x1 in {6} & x2 in NAT & x = [x1,x2] ) or ( ( x1 = 4 or x1 = 5 ) & x2 in QC-symbols A & x = [x1,x2] ) ) by A1, TARSKI:def 2;
then ( ( ( x1 in {4} & x2 in QC-symbols A ) or ( x1 in {5} & x2 in QC-symbols A ) or ( x1 in {6} & x2 in NAT ) ) & x = [x1,x2] ) by TARSKI:def 1;
then ( x in [:{4},(QC-symbols A):] or x in [:{5},(QC-symbols A):] or x in [:{6},NAT:] ) by ZFMISC_1:def 2;
hence ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) by QC_LANG1:def 4, QC_LANG1:def 5, QC_LANG1:def 6; :: thesis: verum

end;

thus ( ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) implies x in QC-variables A ) ; :: thesis: verum