theorem Th7: :: PARTIT_2:7

for R, S being Relation
for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds
R * S is_reflexive_in Y