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 & R .: (dom R) = rng R ) by Th144, Th146;
hence R .: X c= R .: (dom R) ; :: thesis: verum