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