let x be bound_QC-variable; :: thesis: for A being non empty set
for J being interpretation of A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in A holds
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ )
let A be non empty set ; :: thesis: for J being interpretation of A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in A holds
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ )
let J be interpretation of A; :: thesis: for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in A holds
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ )
let S be Element of CQC-Sub-WFF ; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in A holds
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ )
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies for v being Element of Valuations_in A holds
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ ) )
set S1 = CQCSub_All [S,x],xSQ;
assume A1: [S,x] is quantifiable ; :: thesis: for v being Element of Valuations_in A holds
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ )
then CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by Def6;
then (CQCSub_All [S,x],xSQ) `1 = All ([S,x] `2 ),(([S,x] `1 ) `1 ) by A1, Th27;
then (CQCSub_All [S,x],xSQ) `1 = All x,(([S,x] `1 ) `1 ) by MCART_1:7;
then A2: (CQCSub_All [S,x],xSQ) `1 = All x,(S `1 ) by MCART_1:7;
let v be Element of Valuations_in A; :: thesis: ( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ )
consider vS1, vS2 being Val_Sub of A such that
A3: ( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val v,S,x,xSQ) misses dom vS2 ) and
A4: v . (Val_S v,(CQCSub_All [S,x],xSQ)) = v . (((NEx_Val v,S,x,xSQ) +* vS1) +* vS2) by A1, Th90;
( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (((NEx_Val v,S,x,xSQ) +* vS1) +* vS2) |= All x,(S `1 ) ) by A3, Th85;
hence ( J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) iff J,v . (Val_S v,(CQCSub_All [S,x],xSQ)) |= CQCSub_All [S,x],xSQ ) by A4, A2, Def3; :: thesis: verum