theorem Th4: :: NECKLA_3:4
for X being trivial set
for R being Relation of X st not R is empty holds
ex x being object st R = {[x,x]}