let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable 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; :: 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:16;
All x,p is universal by QC_LANG1:def 20;
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:8;
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) by XBOOLE_1:1;
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, XBOOLE_1:1; :: thesis: verum