let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in (All (x,p)) c= Bound_Vars (All (x,p))
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in (All (x,p)) c= Bound_Vars (All (x,p))
let x be bound_QC-variable of Al; :: thesis: ( still_not-bound_in p c= Bound_Vars p implies still_not-bound_in (All (x,p)) c= Bound_Vars (All (x,p)) )
A1: still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:12;
All (x,p) is universal by QC_LANG1:def 21;
then Bound_Vars (All (x,p)) = (Bound_Vars (the_scope_of (All (x,p)))) \/ {(bound_in (All (x,p)))} by SUBSTUT1:6;
then Bound_Vars (All (x,p)) = (Bound_Vars p) \/ {(bound_in (All (x,p)))} by QC_LANG2:7;
then ( (Bound_Vars p) \ {x} c= Bound_Vars p & Bound_Vars p c= Bound_Vars (All (x,p)) ) by XBOOLE_1:7, XBOOLE_1:36;
then A2: (Bound_Vars p) \ {x} c= Bound_Vars (All (x,p)) ;
assume still_not-bound_in p c= Bound_Vars p ; :: thesis: still_not-bound_in (All (x,p)) c= Bound_Vars (All (x,p))
then still_not-bound_in (All (x,p)) c= (Bound_Vars p) \ {x} by A1, XBOOLE_1:33;
hence still_not-bound_in (All (x,p)) c= Bound_Vars (All (x,p)) by A2; :: thesis: verum