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)

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

hence
{ v where v is Dual of L : verum } is non empty Subset of (DivisibleMod L)
by A1; :: thesis: verum
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;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