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

hereby :: according to ALTCAT_1:def 21 :: thesis: EnsCat 1 is trivial

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;

let o1, o2 be Element of (EnsCat 1); :: according to STRUCT_0:def 10 :: thesis: o1 = o2
o1 = {} by A1, TARSKI:def 1;
hence o1 = o2 by A1, TARSKI:def 1; :: thesis: verum