for n being non zero Nat
for a, b being Element of (Divisors_Lattice n) holds
( a "\/" b = a lcm b & a "/\" b = a gcd b )