Green box shows ATP dependencies, black box is Mizar code. Clicking on proof will display the Mizar proof.
<p>Your user agent does not support iframes or is currently configured not to display iframes. However, you may visit <A href="">the related document.</A></p>