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 )

then v in DualSet L ;

hence v in DualLat L by defDualLat; :: thesis: verum

( 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 is Dual of L
; :: thesis: v in DualLat Lassume
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;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

then v in DualSet L ;

hence v in DualLat L by defDualLat; :: thesis: verum