Slate - Intersection is subset of right argument

Library ▹ Essentials ▹ Sets

Proposition 1.1.13. Let U be a set, S, T ⊆ U. Then:

Proof. Let x ∈ S ∩ T.

⇒^def x ∈ T

References.

https://proofwiki.org/wiki/Intersection_is_Subset
http://metamath.tirix.org/inss2.html
https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.inter_subset_right