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 A1: ( [S,x] is quantifiable & 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 ) )
then CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by Def6;
then A2: ( (CQCSub_All [S,x],xSQ) `1 = All ([S,x] `2 ),(([S,x] `1 ) `1 ) & (CQCSub_All [S,x],xSQ) `2 = xSQ ) by A1, Th27;
then A3: (CQCSub_All [S,x],xSQ) `1 = All x,(([S,x] `1 ) `1 ) by MCART_1:7;
then A4: bound_in ((CQCSub_All [S,x],xSQ) `1 ) = x by QC_LANG2:8;
set finSub = RestrictSub (bound_in ((CQCSub_All [S,x],xSQ) `1 )),((CQCSub_All [S,x],xSQ) `1 ),((CQCSub_All [S,x],xSQ) `2 );
A5: 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 A2, A3, A4, MCART_1:7;
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 )));
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 )));
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 ;
A6: 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;
A7: 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;
A8: 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 ))) by XBOOLE_1:7;
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 XXREAL_2:def 7;
then A9: 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 A7, A8, 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 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 rng (RestrictSub (bound_in ((CQCSub_All [S,x],xSQ) `1 )),((CQCSub_All [S,x],xSQ) `1 ),((CQCSub_All [S,x],xSQ) `2 )) by A6, A9;
A11: 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 ))) by XBOOLE_1:7;
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 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 Dom_Bound_Vars (the_scope_of ((CQCSub_All [S,x],xSQ) `1 )) by A7, A11, XBOOLE_0:def 5;
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;
then A13: 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 A12;
(CQCSub_All [S,x],xSQ) `1 = All x,(S `1 ) by A3, MCART_1:7;
then A14: 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 A6, A13, QC_LANG2:8;
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 A1, A4, A5, A10, A14, SUBSTUT1:def 36; :: thesis: verum