What to do

1. Using basic proof skeletons for Mizar, construct and check the proof skeleton for a universally quantified statement (the example below uses the simple verifier (Basic Package) of the Mizar Verifier on Web, click on images to enlarge).

   Now that the theorem has been formalized, start building the proof skeleton.