let M be non countable Aleph; :: thesis: ( M is strongly_inaccessible implies Rank M is Universe )
assume M is strongly_inaccessible ; :: thesis: Rank M is Universe
then ( Rank M is Tarski & Rank M is epsilon-transitive ) by Th37;
hence Rank M is Universe ; :: thesis: verum