let q1, q2 be Element of CQC-WFF ; :: thesis: ( ( for p being Element of CQC-WFF st p = F . a holds
q1 = Ex-the_scope_of p ) & ( for p being Element of CQC-WFF st p = F . a holds
q2 = Ex-the_scope_of p ) implies q1 = q2 )
assume that
A1: for p being Element of CQC-WFF st p = F . a holds
q1 = Ex-the_scope_of p and
A2: for p being Element of CQC-WFF st p = F . a holds
q2 = Ex-the_scope_of p ; :: thesis: q1 = q2
reconsider q = F . a as Element of CQC-WFF ;
q1 = Ex-the_scope_of q by A1;
hence q1 = q2 by A2; :: thesis: verum