theorem Th1: :: WELLSET1:1

for R being Relation
for x being object holds
( x in field R iff ex y being object st
( [x,y] in R or [y,x] in R ) )