let x be object ; :: thesis: for X being set

for R being Relation st x in field (R |_2 X) holds

( x in field R & x in X )

let X be set ; :: thesis: for R being Relation st x in field (R |_2 X) holds

( x in field R & x in X )

let R be Relation; :: thesis: ( x in field (R |_2 X) implies ( x in field R & x in X ) )

A1: ( dom ((X |` R) | X) = (dom (X |` R)) /\ X & rng (X |` (R | X)) = (rng (R | X)) /\ X ) by RELAT_1:61, RELAT_1:88;

assume x in field (R |_2 X) ; :: thesis: ( x in field R & x in X )

then A2: ( x in dom (R |_2 X) or x in rng (R |_2 X) ) by XBOOLE_0:def 3;

A3: ( dom (X |` R) c= dom R & rng (R | X) c= rng R ) by Lm5, RELAT_1:70;

( R |_2 X = (X |` R) | X & R |_2 X = X |` (R | X) ) by Th10, Th11;

then ( ( x in dom (X |` R) & x in X ) or ( x in rng (R | X) & x in X ) ) by A2, A1, XBOOLE_0:def 4;

hence ( x in field R & x in X ) by A3, XBOOLE_0:def 3; :: thesis: verum

for R being Relation st x in field (R |_2 X) holds

( x in field R & x in X )

let X be set ; :: thesis: for R being Relation st x in field (R |_2 X) holds

( x in field R & x in X )

let R be Relation; :: thesis: ( x in field (R |_2 X) implies ( x in field R & x in X ) )

A1: ( dom ((X |` R) | X) = (dom (X |` R)) /\ X & rng (X |` (R | X)) = (rng (R | X)) /\ X ) by RELAT_1:61, RELAT_1:88;

assume x in field (R |_2 X) ; :: thesis: ( x in field R & x in X )

then A2: ( x in dom (R |_2 X) or x in rng (R |_2 X) ) by XBOOLE_0:def 3;

A3: ( dom (X |` R) c= dom R & rng (R | X) c= rng R ) by Lm5, RELAT_1:70;

( R |_2 X = (X |` R) | X & R |_2 X = X |` (R | X) ) by Th10, Th11;

then ( ( x in dom (X |` R) & x in X ) or ( x in rng (R | X) & x in X ) ) by A2, A1, XBOOLE_0:def 4;

hence ( x in field R & x in X ) by A3, XBOOLE_0:def 3; :: thesis: verum