:: deftheorem defines GeneratedRelStr ROUGHS_3:def 4 :
for R being non empty RelStr
for H being Function of (bool the carrier of R),(bool the carrier of R) holds GeneratedRelStr H = RelStr(# the carrier of R,(GeneratedRelation (R,H)) #);