set P = R_ProjCo p;
set R = nabla (EC_SetProjCo (a,b,p));
reconsider PR = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) as Relation of (EC_SetProjCo (a,b,p)) ;
for x being set holds
( x in EC_SetProjCo (a,b,p) iff ex y being set st [x,y] in PR )

proof

let x be set ; :: thesis: ( x in EC_SetProjCo (a,b,p) iff ex y being set st [x,y] in PR )

hereby :: thesis: ( ex y being set st [x,y] in PR implies x in EC_SetProjCo (a,b,p) )

assume AS1: x in EC_SetProjCo (a,b,p) ; :: thesis: ex y being set st [x,y] in PR
then reconsider X = x as Element of ProjCo (GF p) ;
X _EQ_ X ;
then P4: [x,x] in R_ProjCo p ;
[x,x] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by AS1, ZFMISC_1:87;
then [x,x] in PR by P4, XBOOLE_0:def 4;
hence ex y being set st [x,y] in PR ; :: thesis: verum

end;

given y being set such that P1: [x,y] in PR ; :: thesis: x in EC_SetProjCo (a,b,p)
thus x in EC_SetProjCo (a,b,p) by P1, ZFMISC_1:87; :: thesis: verum

end;

then dom PR = EC_SetProjCo (a,b,p) by RELAT_1:def 4;
hence (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p)) by PARTFUN1:def 2, RELAT_2:18, RELAT_2:26; :: thesis: verum