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