set R = R_ProjCo p;
for x being object holds
( x in ProjCo (GF p) iff ex y being object st [x,y] in R_ProjCo p )
proof
let x be object ; :: thesis: ( x in ProjCo (GF p) iff ex y being object st [x,y] in R_ProjCo p )
hereby :: thesis: ( ex y being object st [x,y] in R_ProjCo p implies x in ProjCo (GF p) )
assume x in ProjCo (GF p) ; :: thesis: ex y being object 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 object st [x,y] in R_ProjCo p ; :: thesis: verum
end;
given y being object such that A1: [x,y] in R_ProjCo p ; :: thesis: x in ProjCo (GF p)
consider X, Y being Element of ProjCo (GF p) such that
A2: ( [x,y] = [X,Y] & X _EQ_ Y ) by A1;
x = X by A2, XTUPLE_0:1;
hence x in ProjCo (GF p) ; :: thesis: verum
end;
then dom (R_ProjCo p) = ProjCo (GF p) by XTUPLE_0:def 12;
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 object 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 object ; :: 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
A3: ( [x,y] = [X,Y] & X _EQ_ Y ) ;
( x = X & y = Y ) by A3, XTUPLE_0:1;
hence [y,x] in R_ProjCo p by A3; :: 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 object 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 object ; :: 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 A4: ( 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
A5: ( [x,y] = [X,Y] & X _EQ_ Y ) ;
A6: ( x = X & y = Y ) by A5, XTUPLE_0:1;
consider Y1, Z being Element of ProjCo (GF p) such that
A7: ( [y,z] = [Y1,Z] & Y1 _EQ_ Z ) by A4;
( X _EQ_ Y & Y _EQ_ Z ) by A5, A6, A7, XTUPLE_0:1;
then A8: X _EQ_ Z by Th44;
[x,z] = [X,Z] by A6, A7, XTUPLE_0:1;
hence [x,z] in R_ProjCo p by A8; :: 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