English
If a is related to b and b to c by a transitive relation, then a is related to c.
Русский
Если a связано с b, а b связано с c по транзитивному отношению, то a связано с c.
LaTeX
$$$a \\sim_R b \\to b \\sim_R c \\to a \\sim_R c$$$
Lean4
protected theorem trans [R.IsTrans] (hab : a ~[R] b) (hbc : b ~[R] c) : a ~[R] c :=
trans_of (· ~[R] ·) hab hbc