let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
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 ; :: 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, Def6;
then (CQCSub_All ([S,x],xSQ)) `1 = All (([S,x] `2),(([S,x] `1) `1)) by A1, Th27;
then A4: (CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) by MCART_1:7;
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)) = { i where i is Element of NAT : x. i 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, Th27;
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, MCART_1:7;
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 = min (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)))));
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))) = min (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;
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 NAT ;
A9: min (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))))) = min X by SUBSTUT1:def 11;
( 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)))) & min X 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 XBOOLE_1:7, XXREAL_2:def 7;
then not min (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))))) in Dom_Bound_Vars (the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)) by A9, XBOOLE_0:def 5;
then A10: not x. (min (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)))))) 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, MCART_1:7;
then A11: 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 A8, A10, 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)))) & min X 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 XBOOLE_1:7, XXREAL_2:def 7;
then A12: not min (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))))) 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 A9, 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))) = { i where i is Element of NAT : x. i 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 A13: 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 A8, A12;
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, A13, A11, SUBSTUT1:def 36; :: thesis: verum