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 Th53, Th116; :: according to XBOOLE_0:def 10 :: thesis: R .: X c= (R | Y) .: X
let y be object ; :: 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 object such that
A2: [x1,y] in R and
A3: x1 in X by Def11;
ex x being object 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, Def9; :: thesis: x1 in X
thus x1 in X by A3; :: thesis: verum
end;
hence y in (R | Y) .: X by Def11; :: thesis: verum