:: deftheorem defines = RELAT_1:def 2 :
for P, R being Relation holds
( P = R iff for a, b being object holds
( [a,b] in P iff [a,b] in R ) );