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 & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in 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 A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in 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 A; :: thesis: for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in 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 ; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in 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 A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) implies for v being Element of Valuations_in 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 A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ; :: thesis: for v being Element of Valuations_in 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 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, Th55;
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 Th51;
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 )

proof

assume A6: for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S ; :: thesis: 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
let a be Element of A; :: thesis: J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S
J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S by A6;
hence 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; :: thesis: verum

end;

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 ) implies for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S )

proof

assume A8: 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 A8;
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)));
A9: ( 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, Th31;
A10: ( ( 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, Th72;
A11: ( 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 )

proof

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

end;

A12: ( ( 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 Th76;
hence J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) by Th51; :: thesis: verum

end;

CQCSub_All ([S,x],xSQ) is Sub_universal by A1, Th28;
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, A9, A4, A5, A7, A3, A10, A12, A11, Th29, Th32, Th57, Th75, Th91; :: thesis: verum