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

proof

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

end;

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