The intention of these pages is presentation of thesis, which should be proven in all possible cases occurring during writing Mizar articles. Whenever it is possible, two examples are presented: the first - with a simple definiens, and the second - with a complex one.

In case of Statements possible skeletons of the formulas are presented.

In cases of quite complex thesis (e.g. conjunctions containing 4 conjuncts) thesis are divided into simpler sub-thesis.

Remark: involutiveness, projectivity and idempotence have been not implemented for redefined functors.