let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for vS1 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for vS1 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for vS1 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
let A be non empty set ; :: thesis: for vS1 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
let vS1 be Val_Sub of A,Al; :: thesis: ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) implies for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p )
assume A1: for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ; :: thesis: for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
let y be bound_QC-variable of Al; :: thesis: ( y in (dom vS1) \ {x} implies not y in still_not-bound_in p )
assume A2: y in (dom vS1) \ {x} ; :: thesis: not y in still_not-bound_in p
(dom vS1) \ {x} c= dom vS1 by XBOOLE_1:36;
then not y in still_not-bound_in (All (x,p)) by A1, A2;
then A3: not y in (still_not-bound_in p) \ {x} by QC_LANG3:12;
A4: {x} \/ ((still_not-bound_in p) \ {x}) = {x} \/ (still_not-bound_in p) by XBOOLE_1:39;
not y in {x} by A2, XBOOLE_0:def 5;
then not y in {x} \/ ((still_not-bound_in p) \ {x}) by A3, XBOOLE_0:def 3;
hence not y in still_not-bound_in p by A4, XBOOLE_0:def 3; :: thesis: verum