set A = { v where v is Dual of L : verum } ;
0. (DivisibleMod L) is Dual of L by LmDE0;
then A1: 0. (DivisibleMod L) in { v where v is Dual of L : verum } ;
{ v where v is Dual of L : verum } c= the carrier of (DivisibleMod L)

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { v where v is Dual of L : verum } or v in the carrier of (DivisibleMod L) )
assume v in { v where v is Dual of L : verum } ; :: thesis: v in the carrier of (DivisibleMod L)
then consider v1 being Dual of L such that
B1: v1 = v ;
thus v in the carrier of (DivisibleMod L) by B1; :: thesis: verum

end;

hence { v where v is Dual of L : verum } is non empty Subset of (DivisibleMod L) by A1; :: thesis: verum