let R be Relation; :: thesis: for X, Y being set st X c= Y holds
(R | Y) .: X = R .: X
let X, Y be set ; :: thesis: ( X c= Y implies (R | Y) .: X = R .: X )
assume A1: X c= Y ; :: thesis: (R | Y) .: X = R .: X
thus (R | Y) .: X c= R .: X by Th88, Th157; :: according to XBOOLE_0:def 10 :: thesis: R .: X c= (R | Y) .: X
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: X or y in (R | Y) .: X )
assume y in R .: X ; :: thesis: y in (R | Y) .: X
then consider x1 being set such that
A2: [x1,y] in R and
A3: x1 in X by Def13;
ex x being set st
( [x,y] in R | Y & x in X )

proof

take x1 ; :: thesis: ( [x1,y] in R | Y & x1 in X )
thus [x1,y] in R | Y by A1, A2, A3, Def11; :: thesis: x1 in X
thus x1 in X by A3; :: thesis: verum

end;

hence y in (R | Y) .: X by Def13; :: thesis: verum