let X be set ; :: thesis: for R being Relation holds R .: X = R .: ((dom R) /\ X)
let R be Relation; :: thesis: R .: X = R .: ((dom R) /\ X)
for y being object holds
( y in R .: X iff y in R .: ((dom R) /\ X) )
proof
let y be object ; :: thesis: ( y in R .: X iff y in R .: ((dom R) /\ X) )
thus ( y in R .: X implies y in R .: ((dom R) /\ X) ) :: thesis: ( y in R .: ((dom R) /\ X) implies y in R .: X )
proof
assume y in R .: X ; :: thesis: y in R .: ((dom R) /\ X)
then consider x being object such that
A1: x in dom R and
A2: [x,y] in R and
A3: x in X by Th104;
x in (dom R) /\ X by A1, A3, XBOOLE_0:def 4;
hence y in R .: ((dom R) /\ X) by A2, Def11; :: thesis: verum
end;
assume y in R .: ((dom R) /\ X) ; :: thesis: y in R .: X
then consider x being object such that
x in dom R and
A4: [x,y] in R and
A5: x in (dom R) /\ X by Th104;
x in X by A5, XBOOLE_0:def 4;
hence y in R .: X by A4, Def11; :: thesis: verum
end;
hence R .: X = R .: ((dom R) /\ X) by TARSKI:2; :: thesis: verum