:: deftheorem RIF1Def defines satisfying_RIF1 ROUGHIF1:def 7 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF1 iff for X, Y being Subset of R holds
( f . (X,Y) = 1 iff X c= Y ) );