let Al be QC-alphabet ; 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; 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; 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]; ( [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))
; ( 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))))
;
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; verum