c2 c= c1 +` c2 by CARD_2:94;
hence not c1 +` c2 is empty ; :: thesis: verum