let x be bound_QC-variable; :: thesis:
let S be Element of CQC-Sub-WFF ; :: thesis:
let xSQ be second_Q_comp of [S,x]; :: thesis:
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:
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:8;
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:8;
( 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: