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

( 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