let L be positive-definite RATional Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L) holds
( v in DualLat L iff v is Dual of L )
let v be Vector of (DivisibleMod L); :: thesis: ( v in DualLat L iff v is Dual of L )

hereby :: thesis: ( v is Dual of L implies v in DualLat L )

assume v in DualLat L ; :: thesis: v is Dual of L
then v in DualSet L by defDualLat;
then consider x being Dual of L such that
A1: x = v ;
thus v is Dual of L by A1; :: thesis: verum

end;

assume v is Dual of L ; :: thesis: v in DualLat L
then v in DualSet L ;
hence v in DualLat L by defDualLat; :: thesis: verum