reconsider p = F . a as Element of CQC-WFF ;
take q = Ex-the_scope_of p; :: thesis: for p being Element of CQC-WFF st p = F . a holds
q = Ex-the_scope_of p
thus for p being Element of CQC-WFF st p = F . a holds
q = Ex-the_scope_of p ; :: thesis: verum