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 object holds
( x in EC_SetProjCo (a,b,p) iff ex y being object st [x,y] in PR )
proof
let x be object ; :: thesis: ( x in EC_SetProjCo (a,b,p) iff ex y being object st [x,y] in PR )
hereby :: thesis: ( ex y being object st [x,y] in PR implies x in EC_SetProjCo (a,b,p) )
assume A1: x in EC_SetProjCo (a,b,p) ; :: thesis: ex y being object st [x,y] in PR
then reconsider X = x as Element of ProjCo (GF p) ;
X _EQ_ X ;
then A2: [x,x] in R_ProjCo p ;
[x,x] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by A1, ZFMISC_1:87;
then [x,x] in PR by A2, XBOOLE_0:def 4;
hence ex y being object st [x,y] in PR ; :: thesis: verum
end;
thus ( ex y being object st [x,y] in PR implies x in EC_SetProjCo (a,b,p) ) by ZFMISC_1:87; :: thesis: verum
end;
then dom PR = EC_SetProjCo (a,b,p) by XTUPLE_0:def 12;
hence (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p)) by PARTFUN1:def 2; :: thesis: verum