[mizar] Question about environments

["James Smith" <james.smith@aleph-one.com>]

Good evening,

I've been working on Mizar on and off for a couple of weeks now and I've
made some progress with getting environments right, and learned a little
about the MML library along the way. I've been trying to get the environment
right for the PYTHTRIP article (I'm following Freek Wiedijk's tutorial) and
I have a problem which boils down to the following:

+++

environ

 vocabularies ARYTM, ORDINAL2;
 notations SUBSET_1, ORDINAL1;
 constructors SUBSET_1, ORDINAL1;
 registrations ORDINAL1;
 theorems ORDINAL1;
 requirements SUBSET, BOOLE;

begin

 reserve n for Element of omega;
 n is natural number;            :: This works because of the cluster...
                                 ::   
                                 ::  -> natural Element of omega 
                                 ::   
                                 ::  ...in ORDINAL1, the coherence of which
is 
                                 ::  proved by ORDINAL1:def 13 (which
defines 
                                 ::  'natural' as meaning 'in omega',
essentially
                                 ::  equivalent to 'Element of omega' with
the
                                 ::  requirements SUBSET, BOOLE).

 n in omega;                     :: Again this works because of the
requirements.

 reserve k for natural number;
 
 k in omega by ORDINAL1:def 13;  :: This works
 k in omega;                     :: But this doesn't. Adding ORDINAL1 to the
                                 ::  definitions directive makes no
difference.
::>       *4
 
+++

I would like the assertion 'k in omega' to work without explicit reference
to the relevant definition. Is this possible? 

Previously when I've come across what appear to be insurmountable problems
I've copied the offending lines to the end of existing MML articles and then
wittled down the environments, but when I copy and paste this assertion into
PYTHTRIP, for example, and try to verify it, I get the same *4 error. This
makes me suspect that the assertion can never be accepted without explicit
reference to the definition. Is this true?

Many thanks in advance for any help on this.

Kind regards,

James

http://www.mygarble.com/