rng ([[0]] I) c= {{} } by FUNCOP_1:19;
hence [[0]] I is empty-yielding by RELAT_1:def 15; :: thesis: verum