Theorem: C03S01.Subset.trans (LeanInRome/S3_Logic/S01_Implication_and_the_Universal_Quantifier.lean)

State before:
α : Type u_1
r s t : Set α
⊢ r ⊆ s → s ⊆ t → r ⊆ t
Tactic:
sorry
State after:
no goals