theorem Th6: :: TAXONOM1:6

for X being set
for x, y being object
for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds
[x,y] in R [*]