:: deftheorem GRDef defines GeneratedRelation ROUGHS_3:def 3 :
for R being non empty RelStr
for H being Function of (bool the carrier of R),(bool the carrier of R)
for b₃ being Relation of the carrier of R holds
( b₃ = GeneratedRelation (R,H) iff for x, y being Element of R holds
( [x,y] in b₃ iff x in H . {y} ) );