let M be Aleph; :: thesis: ( GCH & M is inaccessible implies M is strongly_inaccessible )
assume A1: GCH ; :: thesis: ( not M is inaccessible or M is strongly_inaccessible )
assume A2: M is inaccessible ; :: thesis: M is strongly_inaccessible
hence M is regular ; :: according to CARD_FIL:def 15 :: thesis: M is strong_limit
thus M is strong_limit by A1, A2, Th28; :: thesis: verum