∀ {K : Type u_1} {V : Type u_2} {inst : Field K} {inst_1 : AddCommGroup V} {inst_2 : Module K V}
  {carrier : Set (Projectivization K V)}
  {mem_add' :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier →
        Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier}
  {carrier_1 : Set (Projectivization K V)}
  {mem_add'_1 :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier_1 →
        Projectivization.mk K w hw ∈ carrier_1 → Projectivization.mk K (v + w) hvw ∈ carrier_1},
  { carrier := carrier, mem_add' := mem_add' } = { carrier := carrier_1, mem_add' := mem_add'_1 } → carrier = carrier_1