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