[STATEMENT]
lemma domain_subset_carrier[simp]: "domain c \<subseteq> carrier" if "c \<in> charts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain c \<subseteq> carrier
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> charts

goal (1 subgoal):
 1. domain c \<subseteq> carrier
[PROOF STEP]
by (auto simp: carrier_def)