A1: the carrier of (EnsCat 1) = {{}} by Def16, CARD_1:49;

hereby :: according to ALTCAT_1:def 19 :: thesis: EnsCat 1 is 1 -element

let i be object of (EnsCat 1); :: thesis: <^i,i^> is trivial
i = {} by A1, TARSKI:def 1;
hence <^i,i^> is trivial by Def16, Th3; :: thesis: verum

end;

thus the carrier of (EnsCat 1) is 1 -element by A1; :: according to STRUCT_0:def 19 :: thesis: verum