Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019) (Revised by Peter Mazsa, 16-Dec-2021)