theorem Th31: :: RELAT_1:37
for R being Relation st ( for x, y being object holds not [x,y] in R ) holds
R = {} ;