let X, Y be set ; :: thesis: for R being Relation holds (R .: X) \ (R .: Y) c= R .: (X \ Y)
let R be Relation; :: thesis: (R .: X) \ (R .: Y) c= R .: (X \ Y)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R .: X) \ (R .: Y) or y in R .: (X \ Y) )
assume A1: y in (R .: X) \ (R .: Y) ; :: thesis: y in R .: (X \ Y)
then consider x being object such that
A2: [x,y] in R and
A3: x in X by Def11;
not y in R .: Y by A1, XBOOLE_0:def 5;
then ( not x in Y or not [x,y] in R ) by Def11;
then x in X \ Y by A2, A3, XBOOLE_0:def 5;
hence y in R .: (X \ Y) by A2, Def11; :: thesis: verum