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