set RX = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ;

now :: thesis: for x being object st x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } holds
x in [:(ProjCo (GF p)),(ProjCo (GF p)):]

let x be object ; :: thesis: ( x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } implies x in [:(ProjCo (GF p)),(ProjCo (GF p)):] )
assume x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; :: thesis: x in [:(ProjCo (GF p)),(ProjCo (GF p)):]
then consider P, Q being Element of ProjCo (GF p) such that
A1: ( x = [P,Q] & P _EQ_ Q ) ;
thus x in [:(ProjCo (GF p)),(ProjCo (GF p)):] by A1; :: thesis: verum

end;

hence { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p)) by TARSKI:def 3; :: thesis: verum