[STATEMENT]
lemma relation_of_Ndet: "relation_of (P \<sqinter> Q) = ((relation_of P) \<or> (relation_of Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action.relation_of (P \<sqinter> Q) = (action.relation_of P \<or> action.relation_of Q)
[PROOF STEP]
by (simp add: Ndet_def action_of_inverse Ndet_is_CSP)