theorem Th4: :: EQREL_1:4

for X being set holds nabla X is Equivalence_Relation of X