P \/ R c= [:X,Y:] ;
hence P \/ R is Relation of X,Y by Def1; :: thesis: verum