let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )
let x be bound_QC-variable of Al; :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies ( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) ) )
set S1 = CQCSub_All ([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: ( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )
A3: CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by A1, Def5;
then (CQCSub_All ([S,x],xSQ)) `1 = All (([S,x] `2),(([S,x] `1) `1)) by A1, Th26;
then A4: (CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) ;
then A5: bound_in ((CQCSub_All ([S,x],xSQ)) `1) = x by QC_LANG2:7;
set finSub = RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2));
A6: Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)) = { s where s is QC-symbol of Al : x. s in Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)) } by SUBSTUT1:def 9;
(CQCSub_All ([S,x],xSQ)) `2 = xSQ by A1, A3, Th26;
then A7: RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2)) = RestrictSub (x,(All (x,(S `1))),xSQ) by A4, A5;
set Y = (Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))));
set n = upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)));
NSub ((the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)),(RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2)))) = NAT \ ((Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))))) by SUBSTUT1:def 11;
then reconsider X = NAT \ ((Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))))) as non empty Subset of (QC-symbols Al) ;
A8: upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) in NSub ((the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)),(RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))))

proof

upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) = the Element of NSub ((the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)),(RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2)))) by SUBSTUT1:def 12;
hence upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) in NSub ((the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)),(RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2)))) ; :: thesis: verum

end;

( Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)) c= (Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2)))) & upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) in NAT \ ((Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))))) ) by A8, SUBSTUT1:def 11, XBOOLE_1:7;
then not upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) in Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)) by XBOOLE_0:def 5;
then A9: not x. (upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)))) in Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)) by A6;
(CQCSub_All ([S,x],xSQ)) `1 = All (x,(S `1)) by A4;
then A10: not x. (upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)))) in Bound_Vars (S `1) by A9, QC_LANG2:7;
( Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) c= (Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2)))) & upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) in NAT \ ((Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) \/ (Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))))) ) by A8, SUBSTUT1:def 11, XBOOLE_1:7;
then A11: not upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1))) in Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) by XBOOLE_0:def 5;
Sub_Var (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) = { s where s is QC-symbol of Al : x. s in rng (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) } by SUBSTUT1:def 10;
then A12: not x. (upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)))) in rng (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) by A11;
CQCSub_All ([S,x],xSQ) = @ (CQCSub_All ([S,x],xSQ)) by SUBSTUT1:def 35;
hence ( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) ) by A2, A5, A7, A12, A10, SUBSTUT1:def 36; :: thesis: verum