Description: Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019)