set A = 1Cat (0,{0});
take 1Cat ((1Cat (0,{0})),[[(1Cat (0,{0})),(1Cat (0,{0}))],(id (1Cat (0,{0})))]) ; :: thesis: 1Cat ((1Cat (0,{0})),[[(1Cat (0,{0})),(1Cat (0,{0}))],(id (1Cat (0,{0})))]) is Categorial
thus 1Cat ((1Cat (0,{0})),[[(1Cat (0,{0})),(1Cat (0,{0}))],(id (1Cat (0,{0})))]) is Categorial by Th11; :: thesis: verum