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