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