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