let X be set ; :: thesis: for R being Relation st R is well-ordering & X c= field R holds
field (R |_2 X) = X
let R be Relation; :: thesis: ( R is well-ordering & X c= field R implies field (R |_2 X) = X )
assume that
A1: R is well-ordering and
A2: X c= field R ; :: thesis: field (R |_2 X) = X
thus field (R |_2 X) c= X by Th13; :: according to XBOOLE_0:def 10 :: thesis: X c= field (R |_2 X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field (R |_2 X) )
assume A3: x in X ; :: thesis: x in field (R |_2 X)
then A4: [x,x] in [:X,X:] by ZFMISC_1:87;
[x,x] in R by A1, A2, A3, Lm1;
then [x,x] in R |_2 X by A4, XBOOLE_0:def 4;
hence x in field (R |_2 X) by RELAT_1:15; :: thesis: verum