for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_a_model_of_ZF