let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}
let x be bound_QC-variable of A; :: thesis: for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}
defpred S₁[ QC-formula of A] means still_not-bound_in ($1 . x) c= (still_not-bound_in $1) \/ {x};
A1: for p being Element of QC-WFF A st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of QC-WFF A; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:19
.= still_not-bound_in (p . x) by QC_LANG3:7 ;
hence ( S₁[p] implies S₁[ 'not' p] ) by QC_LANG3:7; :: thesis: verum

end;

A2: for p, q being Element of QC-WFF A st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of QC-WFF A; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume that
A3: S₁[p] and
A4: S₁[q] ; :: thesis: S₁[p '&' q]
A5: still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:21
.= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:10 ;
A6: ((still_not-bound_in p) \/ {x}) \/ ((still_not-bound_in q) \/ {x}) = ((still_not-bound_in p) \/ ({x} \/ (still_not-bound_in q))) \/ {x} by XBOOLE_1:4
.= (((still_not-bound_in p) \/ (still_not-bound_in q)) \/ {x}) \/ {x} by XBOOLE_1:4
.= ((still_not-bound_in p) \/ (still_not-bound_in q)) \/ ({x} \/ {x}) by XBOOLE_1:4
.= ((still_not-bound_in p) \/ (still_not-bound_in q)) \/ {x} ;
(still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) c= ((still_not-bound_in p) \/ {x}) \/ ((still_not-bound_in q) \/ {x}) by A3, A4, XBOOLE_1:13;
hence S₁[p '&' q] by A5, A6, QC_LANG3:10; :: thesis: verum

end;

A7: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S₁[p] holds
S₁[ All (x,p)]

proof

let y be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st S₁[p] holds
S₁[ All (y,p)]
let p be Element of QC-WFF A; :: thesis: ( S₁[p] implies S₁[ All (y,p)] )
assume A8: S₁[p] ; :: thesis: S₁[ All (y,p)]

per cases ( y = x or y <> x ) ;

suppose A9: y = x ; :: thesis: S₁[ All (y,p)]

A10: (still_not-bound_in p) \ {x} c= still_not-bound_in p by XBOOLE_1:36;
A11: still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:12;
still_not-bound_in p c= still_not-bound_in (p . x) by Th62;
then still_not-bound_in (All (x,p)) c= still_not-bound_in (p . x) by A11, A10;
then A12: still_not-bound_in (All (x,p)) c= (still_not-bound_in p) \/ {x} by A8, XBOOLE_1:1;
(still_not-bound_in (All (y,p))) \/ {x} = ((still_not-bound_in p) \ {x}) \/ {x} by A9, QC_LANG3:12
.= (still_not-bound_in p) \/ {x} by XBOOLE_1:39 ;
hence S₁[ All (y,p)] by A9, A12, CQC_LANG:24; :: thesis: verum

end;

suppose A13: y <> x ; :: thesis: S₁[ All (y,p)]

A14: (still_not-bound_in (All (y,p))) \/ {x} = ((still_not-bound_in p) \ {y}) \/ {x} by QC_LANG3:12
.= ((still_not-bound_in p) \/ {x}) \ {y} by A13, XBOOLE_1:87, ZFMISC_1:11 ;
still_not-bound_in ((All (y,p)) . x) = still_not-bound_in (All (y,(p . x))) by A13, CQC_LANG:25
.= (still_not-bound_in (p . x)) \ {y} by QC_LANG3:12 ;
hence S₁[ All (y,p)] by A8, A14, XBOOLE_1:33; :: thesis: verum

end;

end;

end;

A15: for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S₁[P ! ll]

proof

let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S₁[P ! ll]
let P be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds S₁[P ! ll]
let ll be QC-variable_list of k,A; :: thesis: S₁[P ! ll]
A16: still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst (ll,((A a. 0) .--> x)))) by CQC_LANG:17
.= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by QC_LANG3:5 ;
still_not-bound_in (Subst (ll,((A a. 0) .--> x))) c= (still_not-bound_in ll) \/ {x} by Th61;
hence S₁[P ! ll] by A16, QC_LANG3:5; :: thesis: verum

end;

A17: still_not-bound_in (VERUM A) = {} by QC_LANG3:3;
(VERUM A) . x = VERUM A by CQC_LANG:15;
then still_not-bound_in ((VERUM A) . x) = {} by A17;
then A18: still_not-bound_in ((VERUM A) . x) c= (still_not-bound_in (VERUM A)) \/ {x} by XBOOLE_1:2;
A19: S₁[ VERUM A] by A18;
thus for h being QC-formula of A holds S₁[h] from QC_LANG1:sch 1(A15, A19, A1, A2, A7); :: thesis: verum