let X be set ; :: thesis: for R being Relation holds R .: X c= R .: (dom R)
let R be Relation; :: thesis: R .: X c= R .: (dom R)
R .: X c= rng R by Th105;
hence R .: X c= R .: (dom R) by Th107; :: thesis: verum