---

Step * 1 1 of Lemma aa_max_w_unit_prop1


1. i : @i
2. x : @i
 j:. ((inl imax(i;x) ) = (inl j ))
BY
{ InstConcl [imax(i;x)] THEN MaAuto }



1.  i  :  \mBbbZ{}@i
2.  x  :  \mBbbZ{}@i
\mvdash{}  \mexists{}j:\mBbbZ{}.  ((inl  imax(i;x)  )  =  (inl  j  ))


By

InstConcl  [\mkleeneopen{}imax(i;x)\mkleeneclose{}]  THEN  MaAuto\mcdot{}



Home Index