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