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
S_Bound (@ (CQCSub_All [S,x],xSQ)) = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(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
S_Bound (@ (CQCSub_All [S,x],xSQ)) = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(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 S_Bound (@ (CQCSub_All [S,x],xSQ)) = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(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: S_Bound (@ (CQCSub_All [S,x],xSQ)) = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(S `1 ))
CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by A1, Def6;
then A3: ( (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 (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: (CQCSub_All [S,x],xSQ) `1 = All x,(([S,x] `1 ) `1 ) by A3, MCART_1:7;
then A6: (CQCSub_All [S,x],xSQ) `1 = All x,(S `1 ) by MCART_1:7;
A7: x = bound_in ((CQCSub_All [S,x],xSQ) `1 ) by A5, QC_LANG2:8;
A8: bound_in ((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 A2, A3, A4, A5, MCART_1:7;
@ (CQCSub_All [S,x],xSQ) = CQCSub_All [S,x],xSQ by SUBSTUT1:def 35;
then S_Bound (@ (CQCSub_All [S,x],xSQ)) = 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 ))) by A8, SUBSTUT1:def 36;
hence S_Bound (@ (CQCSub_All [S,x],xSQ)) = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(S `1 )) by A3, A6, A7, QC_LANG2:8; :: thesis: verum