let C be CategorySet; :: thesis: not C is empty
consider x1, x2, x3, x4, x5 being object such that
A1: C = [x1,x2,x3,x4,x5] by Def3;
assume C is empty ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum