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