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