theorem Th31: :: EQREL_1:31

for X being set
for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}