( a_Type in {a_Type} & [{},0] in [:QuasiLoci,NAT:] ) by ABCMIZ_1:29, TARSKI:def 1, ZFMISC_1:def 2;
hence [a_Type,[{},0]] is Element of Modes by ZFMISC_1:def 2; :: thesis: verum