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 A1: ( [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 ) ) ) ; :: 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 )
set S1 = CQCSub_All [S,x],xSQ;
set p = CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ));
A2: CQCSub_All [S,x],xSQ is Sub_universal by A1, Th28;
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 )
A3: ( 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;
set z = S_Bound (@ (CQCSub_All [S,x],xSQ));
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 ) iff 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

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

end;

thus ( ( 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 ) :: thesis: verum

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 A1; :: thesis: verum

end;

end;

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 ) 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;
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, Th72;
( ( for a being Element of A holds J,(v . (NEx_Val v,S,x,xSQ)) . (x | a) |= S ) iff J,v . (NEx_Val v,S,x,xSQ) |= All x,(S `1 ) )

proof

thus ( ( 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 ) ) :: thesis: ( 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 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;

thus ( 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 ) :: thesis: verum

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;

end;

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, A2, A3, A4, A5, A8, A9, Th29, Th32, Th57, Th75, Th91; :: thesis: verum