theorem Th9: :: OSALG_4:9

{} is Equivalence_Relation of {} by RELSET_1:12;