[STATEMENT]
lemma all_edges_between_disjoint_family_on1:
  assumes "disjoint R"
  shows "disjoint_family_on (\<lambda>X. all_edges_between X Y) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_family_on (\<lambda>X. all_edges_between X Y) R
[PROOF STEP]
by (metis (no_types, lifting) all_edges_between_disjnt1 assms disjnt_def disjoint_family_on_def pairwiseD)