How does one prove there is a Natural number equal to 1 in Mizar (mathematical theorem proving language)?

Hi,

I am very used to hands on tutorials that have me write code immediately so I was trying to do that with mizar. I tried doing the simplest proof I could think of, proving some Nat is 1. I wrote some Mizar but it didn’t work. I linked the code here:

https://stackoverflow.com/questions/53512157/how-does-one-prove-there-is-a-natural-number-equal-to-1-in-mizar-mathematical-t

anyone know whats missing?

Thanks, BM