Enhancement of MIZAR Texts with Transitivity Property of Predicates

A typical proof step in mathematical reasoning consists of two parts - a formula to be proven and a list of references used to justify the formula. In addition, computer proof-assistants can use specialized procedures and algorithms to strengthen their computational power to verify the correctness of reasonings. The Mizar system supports several mechanisms to increase automation of some reasoning steps. One of them is registration of chosen properties of predicates and functors when they are defined. We propose strengthening of the Mizar system by processing another common property used in mathematics - transitivity.