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

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