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 ) )

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

( 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 that 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;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

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