set L = Divisors_Lattice n;
TT: ex c being Element of (Divisors_Lattice n) st
for a being Element of (Divisors_Lattice n) holds
( c "\/" a = c & a "\/" c = c )
proof
n in NatDivisors n by MOEBIUS1:39;
then reconsider c = n as Element of (Divisors_Lattice n) by DivLat;
take c ; :: thesis: for a being Element of (Divisors_Lattice n) holds
( c "\/" a = c & a "\/" c = c )
let a be Element of (Divisors_Lattice n); :: thesis: ( c "\/" a = c & a "\/" c = c )
a in the carrier of (Divisors_Lattice n) ;
then a in NatDivisors n by DivLat;
hence ( c "\/" a = c & a "\/" c = c ) by NEWTON:44, MOEBIUS1:39; :: thesis: verum
end;
ex c being Element of (Divisors_Lattice n) st
for a being Element of (Divisors_Lattice n) holds
( c "/\" a = c & a "/\" c = c )
proof
1 in NatDivisors n by MOEBIUS1:39, NAT_D:6;
then reconsider c = 1 as Element of (Divisors_Lattice n) by DivLat;
take c ; :: thesis: for a being Element of (Divisors_Lattice n) holds
( c "/\" a = c & a "/\" c = c )
thus for a being Element of (Divisors_Lattice n) holds
( c "/\" a = c & a "/\" c = c ) by NEWTON:51; :: thesis: verum
end;
then t1: ( Divisors_Lattice n is lower-bounded & Divisors_Lattice n is upper-bounded ) by TT;
for a, b, c being Element of (Divisors_Lattice n) holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
proof
let a, b, c be Element of (Divisors_Lattice n); :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
a in the carrier of (Divisors_Lattice n) ;
then a1: a in NatDivisors n by DivLat;
b in the carrier of (Divisors_Lattice n) ;
then a2: b in NatDivisors n by DivLat;
c in the carrier of (Divisors_Lattice n) ;
then c in NatDivisors n by DivLat;
then reconsider n1 = a, n2 = b, n3 = c as non zero Nat by a1, a2;
(n3 gcd n1) lcm (n2 gcd n1) = (n3 lcm n2) gcd n1 by INT_4:46;
hence a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; :: thesis: verum
end;
hence ( Divisors_Lattice n is distributive & Divisors_Lattice n is bounded ) by t1; :: thesis: verum