A1: the carrier of (EnsCat {0}) = {0} by Def14;
hereby :: according to ALTCAT_1:def 19 :: thesis: EnsCat {0} is 1 -element
let i be Object of (EnsCat {0}); :: thesis: <^i,i^> is trivial
i = 0 by A1, TARSKI:def 1;
hence <^i,i^> is trivial by Def14, FUNCT_2:127; :: thesis: verum
end;
thus the carrier of (EnsCat {0}) is 1 -element by A1; :: according to STRUCT_0:def 19 :: thesis: verum