Sketch the formalization of Theorem 1 in reference [1, p.544] in the related reading in:

• natural language and
• formalized (Mizar) language

[ Back ]