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