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 & not a in Im (R ` ),x ) by Th25;
[x,a] in R by A2, 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 A3: a in (R ` ) .:^ X ; :: thesis: a in (R .: X) `
A4: ( 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 A5: x in X ; :: thesis: not [x,a] in R
assume A6: [x,a] in R ; :: thesis: contradiction
a in Im (R ` ),x by A3, A5, Th24;
then consider b being set such that
A7: ( [b,a] in R ` & b in {x} ) by RELAT_1:def 13;
A8: ( [x,a] in R ` & [x,a] in R ) by A6, A7, TARSKI:def 1;
R ` misses R by XBOOLE_1:79;
hence contradiction by 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 A3; :: thesis: verum

end;

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

then consider y being set such that
A10: ( [y,a] in R & y in X ) by RELAT_1:def 13;
thus contradiction by A3, A4, A10; :: thesis: verum

end;

end;