Managing Heterogeneous Theories within a Mathematical Knowledge Repository

The problem of the integrity of a computer managed mathematical knowledge repository is in the heart of MKM since mathematical vernacular is a language permitting plenty of ways in expressing the same meaning. The users of the library are naturally forced to choose certain way among many similar ones, unless different approaches are provided by developers. Mizar is a system for formalizing mathematical content which is sufficient mature and flexible for a coexistence of different approaches of concrete subjects. Considering Mizar formalizations of ortholattice theory we discuss a useful mechanism of coping with the heterogeneity of theories in a library of mathematical facts.