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 by Th36;
hence Rank M is Universe ; :: thesis: verum