A1: C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2 by Th72;
reconsider E = OrdC0-> C2 as Functor of ((OrdC 0) [x] C1),C2 ;
OrdC 0,E is_exponent_of C1,C2 by Lm7;
hence C2 |^ C1 is empty by CAT_7:15, A1, Th73; :: thesis: verum