let M be non countable Aleph; :: thesis: ( M is strongly_inaccessible implies Rank M is being_a_model_of_ZF )
assume M is strongly_inaccessible ; :: thesis: Rank M is being_a_model_of_ZF
then A1: Rank M is Universe by CARD_LAR:38;
omega c= M ;
then omega c< M ;
then A2: omega in M by ORDINAL1:11;
M c= Rank M by CLASSES1:38;
hence Rank M is being_a_model_of_ZF by A1, A2, Th6; :: thesis: verum