( 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