theorem Th1: :: WELLORD1:1

for a, x being object
for R being Relation holds
( x in R -Seg a iff ( x <> a & [x,a] in R ) )