A1: C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2 by Th72;
reconsider E = OrdC0-> C2 as Functor of ((OrdC 1) [x] C1),C2 ;
OrdC 1,E is_exponent_of C1,C2 by Lm8;
then C2 |^ C1 ~= OrdC 1 by A1, Th73;
hence ( not C2 |^ C1 is empty & C2 |^ C1 is trivial ) by Th27; :: thesis: verum