set R = R_ProjCo p;
for x being set holds
( x in ProjCo (GF p) iff ex y being set st [x,y] in R_ProjCo p )

proof

let x be set ; :: thesis: ( x in ProjCo (GF p) iff ex y being set st [x,y] in R_ProjCo p )

hereby :: thesis: ( ex y being set st [x,y] in R_ProjCo p implies x in ProjCo (GF p) )

assume x in ProjCo (GF p) ; :: thesis: ex y being set st [x,y] in R_ProjCo p
then reconsider X = x as Element of ProjCo (GF p) ;
X _EQ_ X ;
then [x,x] in R_ProjCo p ;
hence ex y being set st [x,y] in R_ProjCo p ; :: thesis: verum

end;

given y being set such that P1: [x,y] in R_ProjCo p ; :: thesis: x in ProjCo (GF p)
consider X, Y being Element of ProjCo (GF p) such that
P2: ( [x,y] = [X,Y] & X _EQ_ Y ) by P1;
x = X by P2, ZFMISC_1:27;
hence x in ProjCo (GF p) ; :: thesis: verum

end;

then dom (R_ProjCo p) = ProjCo (GF p) by RELAT_1:def 4;
hence R_ProjCo p is total by PARTFUN1:def 2; :: thesis: ( R_ProjCo p is symmetric & R_ProjCo p is transitive )
for x, y being set st x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p holds
[y,x] in R_ProjCo p

proof

let x, y be set ; :: thesis: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p implies [y,x] in R_ProjCo p )
assume ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p ) ; :: thesis: [y,x] in R_ProjCo p
then consider X, Y being Element of ProjCo (GF p) such that
P1: ( [x,y] = [X,Y] & X _EQ_ Y ) ;
( x = X & y = Y ) by P1, ZFMISC_1:27;
hence [y,x] in R_ProjCo p by P1; :: thesis: verum

end;

then R_ProjCo p is_symmetric_in field (R_ProjCo p) by RELAT_2:def 3;
hence R_ProjCo p is symmetric by RELAT_2:def 11; :: thesis: R_ProjCo p is transitive
for x, y, z being set st x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p holds
[x,z] in R_ProjCo p

proof

let x, y, z be set ; :: thesis: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p implies [x,z] in R_ProjCo p )
assume AS1: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p ) ; :: thesis: [x,z] in R_ProjCo p
then consider X, Y being Element of ProjCo (GF p) such that
P1: ( [x,y] = [X,Y] & X _EQ_ Y ) ;
P2: ( x = X & y = Y ) by P1, ZFMISC_1:27;
consider Y1, Z being Element of ProjCo (GF p) such that
P3: ( [y,z] = [Y1,Z] & Y1 _EQ_ Z ) by AS1;
( X _EQ_ Y & Y _EQ_ Z ) by P1, P2, P3, ZFMISC_1:27;
then P5: X _EQ_ Z by LmEQV3;
[x,z] = [X,Z] by P2, P3, ZFMISC_1:27;
hence [x,z] in R_ProjCo p by P5; :: thesis: verum

end;

then R_ProjCo p is_transitive_in field (R_ProjCo p) by RELAT_2:def 8;
hence R_ProjCo p is transitive by RELAT_2:def 16; :: thesis: verum