English
The strict subset relation is transitive when composed with itself: if S ⊊ T and T ⊊ U, then S ⊊ U.
Русский
Строгое подмножество сохраняет транзитивность при повторной композиции: если S ⊊ T и T ⊊ U, то S ⊊ U.
LaTeX
$$$\\forall S,T,U\\subseteq\\alpha, (S\\subset T) \\land (T\\subset U) \\Rightarrow (S\\subset U)$$$
Lean4
instance : Trans ((· ⊂ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·) :=
show Trans (· < ·) (· < ·) (· < ·) by infer_instance