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

assume M is strongly_inaccessible ; :: thesis: Rank M is Universe

then Rank M is Tarski by Th36;

hence Rank M is Universe ; :: thesis: verum