---

Step * of Lemma isect2-record

∀[T1,T2:Atom ⟶ Type].
  ((record(x.T1[x]) ⋂ record(x.T2[x]) ⊆r record(x.T1[x] ⋂ T2[x]))
  ∧ (record(x.T1[x] ⋂ T2[x]) ⊆r record(x.T1[x]) ⋂ record(x.T2[x])))
BY
{ Auto }

1
1. T1 : Atom ⟶ Type
2. T2 : Atom ⟶ Type
⊢ record(x.T1[x]) ⋂ record(x.T2[x]) ⊆r record(x.T1[x] ⋂ T2[x])

---

Latex:

---

Latex:
\mforall{}[T1,T2:Atom  {}\mrightarrow{}  Type].
    ((record(x.T1[x])  \mcap{}  record(x.T2[x])  \msubseteq{}r  record(x.T1[x]  \mcap{}  T2[x]))
    \mwedge{}  (record(x.T1[x]  \mcap{}  T2[x])  \msubseteq{}r  record(x.T1[x])  \mcap{}  record(x.T2[x])))


By

---

Latex:
Auto

---

Home Index