let a be object ; :: thesis: for R being Relation holds R -Seg a c= field R

let R be Relation; :: thesis: R -Seg a c= field R

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in R -Seg a or b in field R )

assume b in R -Seg a ; :: thesis: b in field R

then [b,a] in R by Th1;

hence b in field R by RELAT_1:15; :: thesis: verum

let R be Relation; :: thesis: R -Seg a c= field R

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in R -Seg a or b in field R )

assume b in R -Seg a ; :: thesis: b in field R

then [b,a] in R by Th1;

hence b in field R by RELAT_1:15; :: thesis: verum