let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) 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 Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let J be interpretation of Al,A; :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) 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 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) implies for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) ) )
assume that
A1: [S,x] is quantifiable and
A2: for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ; :: thesis: for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
set S1 = CQCSub_All ([S,x],xSQ);
set z = S_Bound (@ (CQCSub_All ([S,x],xSQ)));
A3: ( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) iff for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S ) by A1, Th54;
set q = CQC_Sub S;
A4: ( J,v |= All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S)) iff for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S ) by Th50;
A5: ( ( for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S ) implies for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) by A2;
A6: ( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) implies for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S )

proof

assume A7: for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ; :: thesis: for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S
let a be Element of A; :: thesis: J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S
J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S by A7;
hence J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S by A2; :: thesis: verum

end;

set p = CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)));
A8: ( J,v |= CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) iff J,v |= CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) ) by A1, Th30;
A9: ( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S ) iff for a being Element of A holds J,v . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S ) by A1, Th70;
A10: ( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) implies for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S ) by Th50;
A11: ( ( for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S ) implies J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) )

proof

assume for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S ; :: thesis: J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1))
then for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S `1 by Th73;
hence J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) by Th50; :: thesis: verum

end;

CQCSub_All ([S,x],xSQ) is Sub_universal by A1, Th27;
hence ( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) ) by A1, A8, A4, A5, A6, A3, A9, A11, A10, Th28, Th31, Th56, Th72, Th87; :: thesis: verum