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

hereby :: thesis: ( x <> a & [x,a] in R implies x in R -Seg a )

assume A1: x in R -Seg a ; :: thesis: ( x <> a & [x,a] in R )
hence x <> a by ZFMISC_1:56; :: thesis: [x,a] in R
ex y being object st
( [x,y] in R & y in {a} ) by A1, RELAT_1:def 14;
hence [x,a] in R by TARSKI:def 1; :: thesis: verum

end;

assume that
A2: x <> a and
A3: [x,a] in R ; :: thesis: x in R -Seg a
a in {a} by TARSKI:def 1;
then x in Coim (R,a) by A3, RELAT_1:def 14;
hence x in R -Seg a by A2, ZFMISC_1:56; :: thesis: verum