[mizar] Studying Mizar

[Boris Schminke <schminkeba@gmail.com>]

Dear All,
I'm writing to ask for advise in studying Mizar.
I think that Mizar is great and I have been trying to study it for
some time and now I understand syntax or at least proof's structures
better than I used to do several months ago. The problem is that I
still do not understand the whole logic of MML. For example, when I
tried to prove some theorems from XBOOLE_1 article I faced no
difficulty, but in great contrast to it, I do not understand a word
from INTEGR1C and even XCMLPX_0 appears to be not very obvious for me.
For instance, why imaginary unit <i> is the same as (0,1) --> (0,1) or
even worse what does --> mean, since (0,1) somehow resembles the
definition of imaginary unit I am used to.
What should I do? Maybe it would be better to read or even write
proofs for some amount of 'core' articles of MML? If so, then couldn't
anybody said me, what exactly? Or maybe it's better to try to
understand at last the INTEGR1C lurking the MML far and wide? I've
tried to use MML Query but still the notions and names used in MML are
not always the same with ones in my head. In MML there are 'bags',
'Go-boards' and other unusual objects. I will be very glad if somebody
tells me how I can my best to comprehend the logic of MML.
I'm looking forward to hearing from you.
Yours,
Schminke Boris.