let A be QC-alphabet ; 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 ; ( 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 )
( ( 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
;
( 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;
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 )
; verum