Description: Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021)