let R1, R2 be Relation of the carrier of CPS,(ProjectiveLines CPS); :: thesis: ( ( for x, y being object holds
( [x,y] in R1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) & ( for x, y being object holds
( [x,y] in R2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) implies R1 = R2 )
assume that
A1: for x, y being object holds
( [x,y] in R1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) and
A2: for x, y being object holds
( [x,y] in R2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ; :: thesis: R1 = R2

now :: thesis: for x, y being object holds
( [x,y] in R1 iff [x,y] in R2 )

let x, y be object ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )

A3: now :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

assume A4: [x,y] in R2 ; :: thesis: [x,y] in R1
then A5: ex Y being set st
( y = Y & x in Y ) by A2;
( x in the carrier of CPS & y in ProjectiveLines CPS ) by A2, A4;
hence [x,y] in R1 by A1, A5; :: thesis: verum

end;

now :: thesis: ( [x,y] in R1 implies [x,y] in R2 )

assume A6: [x,y] in R1 ; :: thesis: [x,y] in R2
then A7: ex Y being set st
( y = Y & x in Y ) by A1;
( x in the carrier of CPS & y in ProjectiveLines CPS ) by A1, A6;
hence [x,y] in R2 by A2, A7; :: thesis: verum

end;

hence ( [x,y] in R1 iff [x,y] in R2 ) by A3; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum