:: deftheorem defines -Seg WELLORD1:def 1 :
for R being Relation
for a being object holds R -Seg a = (Coim (R,a)) \ {a};