let A, B be set ; :: thesis: for X being Subset of A
for R being Relation of A,B holds (R .: X) ` = (R ` ) .:^ X
let X be Subset of A; :: thesis: for R being Relation of A,B holds (R .: X) ` = (R ` ) .:^ X
let R be Relation of A,B; :: thesis: (R .: X) ` = (R ` ) .:^ X
thus (R .: X) ` c= (R ` ) .:^ X :: according to XBOOLE_0:def 10 :: thesis: (R ` ) .:^ X c= (R .: X) `

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (R .: X) ` or a in (R ` ) .:^ X )
assume A1: a in (R .: X) ` ; :: thesis: a in (R ` ) .:^ X
then reconsider B = B as non empty set ;
reconsider a = a as Element of B by A1;
assume not a in (R ` ) .:^ X ; :: thesis: contradiction
then consider x being set such that
A2: x in X and
A3: not a in Im (R ` ),x by Th25;
[x,a] in R by A2, A3, Th42;
then a in R .: X by A2, RELAT_1:def 13;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (R ` ) .:^ X or a in (R .: X) ` )
assume A4: a in (R ` ) .:^ X ; :: thesis: a in (R .: X) `
A5: ( a in (R ` ) .:^ X implies for x being set st x in X holds
not [x,a] in R )

proof

assume a in (R ` ) .:^ X ; :: thesis: for x being set st x in X holds
not [x,a] in R
let x be set ; :: thesis: ( x in X implies not [x,a] in R )
assume A6: x in X ; :: thesis: not [x,a] in R
assume A7: [x,a] in R ; :: thesis: contradiction
a in Im (R ` ),x by A4, A6, Th24;
then ex b being set st
( [b,a] in R ` & b in {x} ) by RELAT_1:def 13;
then A8: [x,a] in R ` by TARSKI:def 1;
R ` misses R by XBOOLE_1:79;
hence contradiction by A7, A8, XBOOLE_0:3; :: thesis: verum

end;

assume A9: not a in (R .: X) ` ; :: thesis: contradiction

per cases ( not a in B or a in R .: X ) by A9, XBOOLE_0:def 5;

suppose not a in B ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose a in R .: X ; :: thesis: contradiction

then ex y being set st
( [y,a] in R & y in X ) by RELAT_1:def 13;
hence contradiction by A4, A5; :: thesis: verum

end;

end;