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