English
The transitivity axiom holds: if a relates to b and b relates to c, then a relates to c in PreEnvelGroupRel.
Русский
Транзитивность: если a связано с b и b связано с c, то a связано с c.
LaTeX
$$$\forall a,b,c:\ PreEnvelGroupRel\ a\ b \Rightarrow PreEnvelGroupRel\ b\ c \Rightarrow PreEnvelGroupRel\ a\ c.$$$
Lean4
@[trans]
theorem trans {R : Type u} [Rack R] {a b c : PreEnvelGroup R} :
PreEnvelGroupRel R a b → PreEnvelGroupRel R b c → PreEnvelGroupRel R a c
| ⟨rab⟩, ⟨rbc⟩ => (rab.trans rbc).rel