take L = ZeroCLC V; :: thesis: Carrier L c= A
thus Carrier L c= A ; :: thesis: verum