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 object ; :: 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, Th41;
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 object ; :: 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 object 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 object st
( [y,a] in R & y in X ) by RELAT_1:def 13;
hence contradiction by A4, A5; :: thesis: verum
end;
end;