take L = ZeroLC V; :: thesis: Carrier L c= A
Carrier L = {} by Def5;
hence Carrier L c= A ; :: thesis: verum