take L = Z_ZeroLC V; :: thesis: Carrier L c= A
Carrier L = {} by Def20;
hence Carrier L c= A ; :: thesis: verum