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 Th111;
hence R .: X c= R .: (dom R) by Th113; :: thesis: verum