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