for M being non limit_cardinal Aleph ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M