theorem :: EQREL_1:8

for X being set
for R being reflexive total Relation of X st ex x being set st x in X holds
R <> {} ;