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