theorem Th7: :: TOLER_1:7

for X being set
for x being object
for T being reflexive total Relation of X holds
( x in X iff [x,x] in T )