let x be object ; :: thesis: for R being Relation holds
( x in field R or R -Seg x = {} )
let R be Relation; :: thesis: ( x in field R or R -Seg x = {} )
assume A1: not x in field R ; :: thesis: R -Seg x = {}
set y = the Element of R -Seg x;
assume R -Seg x <> {} ; :: thesis: contradiction
then [ the Element of R -Seg x,x] in R by Th1;
hence contradiction by A1, RELAT_1:15; :: thesis: verum