let L be Z_Lattice; :: thesis: for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT ) holds

L is RATional

let I be Basis of L; :: thesis: ( ( for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT ) implies L is RATional )

assume A1: for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT ; :: thesis: L is RATional

for v, u being Vector of L holds <;v,u;> in RAT by A1, ThRatLat1A;

hence L is RATional by ZMODLAT2:def 1; :: thesis: verum

<;v,u;> in RAT ) holds

L is RATional

let I be Basis of L; :: thesis: ( ( for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT ) implies L is RATional )

assume A1: for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT ; :: thesis: L is RATional

for v, u being Vector of L holds <;v,u;> in RAT by A1, ThRatLat1A;

hence L is RATional by ZMODLAT2:def 1; :: thesis: verum